A Deep Inference System for Differential Linear Logic

Matteo Acclavio, Giulio Guerrieri

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

2 Citations (SciVal)

Abstract

Differential linear logic (DiLL) provides a fine analysis of resource consumption in cut-elimination. We investigate the subsystem of DiLL without promotion in a deep inference formalism, where cuts are at an atomic level. In our system every provable formula admits a derivation in normal form, via a normalization procedure that commutes with the translation from sequent calculus to deep inference.

Original languageEnglish
Title of host publicationProceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications
Pages26-49
Number of pages24
Publication statusPublished - 30 Dec 2021
Externally publishedYes
Event2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020 - Virtual, Online
Duration: 29 Jun 202030 Jun 2020

Publication series

NameElectronic Proceedings in Theoretical Computer Science, EPTCS
PublisherOpen Publishing Association
Volume353
ISSN (Print)2075-2180

Conference

Conference2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020
CityVirtual, Online
Period29/06/2030/06/20

Acknowledgements

The authors thank Andrea Aler Tubella, Alessio Guglielmi, Lutz Straßburger and the anonymous reviewers for their insightful comments.

Funding

This work has been partially supported by the EPSRC grant EP/R029121/1

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'A Deep Inference System for Differential Linear Logic'. Together they form a unique fingerprint.

Cite this