Abstract
Realizability methods allowed to prove normalization results on many typed calculi. Girard adapted these methods to systems of nets and managed to prove normalization of second order Linear Logic [4]. Our contribution is to provide an extension of this proof that embrace Full Differential Linear Logic (a logic that can describe both single-use resources and inexhaustible resources). Anchored within the realizability framework our proof is modular enough so that further extensions (to second order, to additive constructs or to any other independent feature that can be dealt with using realizability) come for free.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ehrhard, T., Regnier, L.: The differential lambda-calculus. In: TCS, vol. 309, pp. 1–41. Elsevier Science Publishers Ltd., Amsterdam (2004)
Ehrhard, T., Regnier, L.: Differential interaction nets. In: TCS, vol. 364, pp. 166–195. Elsevier Science Publishers Ltd., Amsterdam (2006)
Ehrhard, T., Regnier, L.: Uniformity and the Taylor expansion of ordinary lambda-terms. In: TCS, vol. 403, pp. 347–372. Elsevier Science Publishers Ltd., Amsterdam (2008)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Lafont, Y.: Interaction nets. In: Principles of Programming Languages, pp. 95–108. ACM, New York (1990)
Lafont, Y.: From proof nets to interaction nets. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 225–247. Cambridge University Press, Cambridge (1995)
Pagani, M.: The Cut-Elimination Thereom for Differential Nets with Boxes. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 219–233. Springer, Heidelberg (2009)
Pagani, M., de Falco, L.T.: Strong Normalization Property for Second Order Linear Logic. Theoretical Computer Science 411(2), 410–444 (2010)
Tranquilli, P.: Intuitionistic differential nets and lambda-calculus. Theoretical Computer Science 412(20), 1979–1997 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gimenez, S. (2011). Realizability Proof for Normalization of Full Differential Linear Logic. In: Ong, L. (eds) Typed Lambda Calculi and Applications. TLCA 2011. Lecture Notes in Computer Science, vol 6690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21691-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-21691-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21690-9
Online ISBN: 978-3-642-21691-6
eBook Packages: Computer ScienceComputer Science (R0)