Abstract
Recently Ehrhard and Regnier have introduced Differential Linear Logic, DiLL for short — an extension of the Multiplicative Exponential fragment of Linear Logic that is able to express non-deterministic computations. The authors have examined the cut-elimination of the promotion-free fragment of DiLL by means of a proofnet-like calculus: differential interaction nets. We extend this analysis to exponential boxes and prove the Cut-Elimination Theorem for the whole DiLL: every differential net that is sequentializable can be reduced to a cut-free net.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Danos, V.: La Logique Linéaire appliquée à l’étude de divers processus de normalisation (principalement du λ-calcul). Thèse de doctorat, Université Paris VII (1990)
Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28, 181–203 (1989)
Ehrhard, T., Laurent, O.: Interpreting a finitary pi-calculus in differential interaction nets. Submitted journal version (April 2008)
Ehrhard, T., Regnier, L.: Differential interaction nets. Theor. Comput. Sci. 364(2), 166–195 (2006)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Lafont, Y.: Interaction nets. In: POPL 1990: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 95–108. ACM Press, New York (1990)
Pagani, M.: Acyclicity and coherence in multiplicative and exponential linear logic. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 531–545. Springer, Heidelberg (2006)
Pagani, M., de Falco, L.T.: Strong normalization property for second order linear logic. Pre-print, Istituto per la Applicazioni del Calcolo, Roma (2007); To appear in Theoretical Computer Science
Vaux, L.: λ-calcul différentiel et logique classique: interactions calculatoires. Thèse de doctorat, Université Aix-Marseille II (November 2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pagani, M. (2009). The Cut-Elimination Theorem for Differential Nets with Promotion. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-02273-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02272-2
Online ISBN: 978-3-642-02273-9
eBook Packages: Computer ScienceComputer Science (R0)