A Deep Inference System for Differential Linear Logic

Matteo Acclavio
(University of Luxembourg, Belval, Luxembourg)
Giulio Guerrieri
(University of Bath, Department of Computer Science, Bath, United Kingdom)

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.

In Ugo Dal Lago and Valeria de Paiva: Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity&TLLA 2020), Online, 29-30 June 2020, Electronic Proceedings in Theoretical Computer Science 353, pp. 26–49.
Published: 30th December 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.353.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org