A Deep Inference System for Differential Linear Logic

Matteo Acclavio; Giulio Guerrieri

doi:10.4204/EPTCS.353.2

A Deep Inference System for Differential Linear Logic

Matteo Acclavio, Giulio Guerrieri

Research output: Contribution to journal › Conference article › peer-review

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
Pages (from-to)	26-49
Number of pages	24
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	353
DOIs	https://doi.org/10.4204/EPTCS.353.2
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

ASJC Scopus subject areas

Software

Access to Document

10.4204/EPTCS.353.2

Cite this

@article{53f08c59ce034699b6051f8168cd1d28,

title = "A Deep Inference System for Differential Linear Logic",

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.",

author = "Matteo Acclavio and Giulio Guerrieri",

note = "Funding Information: Acknowledgments. The authors thank Andrea Aler Tubella, Alessio Guglielmi, Lutz Stra{\ss}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”. ; 2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020 ; Conference date: 29-06-2020 Through 30-06-2020",

year = "2021",

month = dec,

day = "30",

doi = "10.4204/EPTCS.353.2",

language = "English",

volume = "353",

pages = "26--49",

journal = "Electronic Proceedings in Theoretical Computer Science",

issn = "2075-2180",

publisher = "Open Publishing Association",

}

TY - JOUR

T1 - A Deep Inference System for Differential Linear Logic

AU - Acclavio, Matteo

AU - Guerrieri, Giulio

N1 - 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”.

PY - 2021/12/30

Y1 - 2021/12/30

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85122425016&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.353.2

DO - 10.4204/EPTCS.353.2

M3 - Conference article

AN - SCOPUS:85122425016

VL - 353

SP - 26

EP - 49

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

T2 - 2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020

Y2 - 29 June 2020 through 30 June 2020

ER -

A Deep Inference System for Differential Linear Logic

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this