Projects per year
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 language | English |
---|---|
Title of host publication | Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications |
Pages | 26-49 |
Number of pages | 24 |
Publication status | Published - 30 Dec 2021 |
Externally published | Yes |
Event | 2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020 - Virtual, Online Duration: 29 Jun 2020 → 30 Jun 2020 |
Publication series
Name | Electronic Proceedings in Theoretical Computer Science, EPTCS |
---|---|
Publisher | Open Publishing Association |
Volume | 353 |
ISSN (Print) | 2075-2180 |
Conference
Conference | 2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020 |
---|---|
City | Virtual, Online |
Period | 29/06/20 → 30/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.Projects
- 1 Finished
-
Typed Lambda-Calculi with Sharing and Unsharing
Heijltjes, W. (PI)
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council