A Deep Inference System for Differential Linear Logic

Matteo Acclavio; Giulio Guerrieri

A Deep Inference System for Differential Linear Logic

Matteo Acclavio, Giulio Guerrieri

Université du Luxembourg

Research output: Chapter or section in a book/report/conference proceeding › Chapter 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 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

Access to Document

Cite this

A Deep Inference System for Differential Linear Logic. / Acclavio, Matteo; Guerrieri, Giulio.
Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications. 2021. p. 26-49 (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 353).

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

Acclavio, M & Guerrieri, G 2021, A Deep Inference System for Differential Linear Logic. in Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications. Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 353, pp. 26-49, 2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020, Virtual, Online, 29/06/20. <https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?TLLALINEARITY2020.2>

@inproceedings{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",

year = "2021",

month = dec,

day = "30",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

publisher = "Open Publishing Association",

pages = "26--49",

booktitle = "Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications",

note = "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",

}

TY - GEN

T1 - A Deep Inference System for Differential Linear Logic

AU - Acclavio, Matteo

AU - Guerrieri, Giulio

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

M3 - Chapter in a published conference proceeding

AN - SCOPUS:85122425016

T3 - Electronic Proceedings in Theoretical Computer Science, EPTCS

SP - 26

EP - 49

BT - Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications

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

Publication series

Conference

Acknowledgements

Funding

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

A Deep Inference System for Differential Linear Logic

Abstract

Publication series

Conference

Acknowledgements

Funding

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this