A Deep Inference System for Differential Linear Logic

Matteo Acclavio, Giulio Guerrieri

Research output: Contribution to journalConference articlepeer-review

2 Citations (SciVal)


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
Pages (from-to)26-49
Number of pages24
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
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

Bibliographical note

Funding Information:
Acknowledgments. The authors thank Andrea Aler Tubella, Alessio Guglielmi, Lutz Straßburger and the anonymous reviewers for their insightful comments. This work has been partially supported by the EPSRC grant EP/R029121/1 “Typed Lambda-Calculi with Sharing and Unsharing”.

ASJC Scopus subject areas

  • Software

Cite this