A Deep Inference System for Differential Linear Logic
Logic in Computer Science
2022-01-03 v1
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.
Cite
@article{arxiv.2112.14963,
title = {A Deep Inference System for Differential Linear Logic},
author = {Matteo Acclavio and Giulio Guerrieri},
journal= {arXiv preprint arXiv:2112.14963},
year = {2022}
}
Comments
In Proceedings Linearity&TLLA 2020, arXiv:2112.14305