Realizability Proof for Normalization of Full Differential Linear Logic

  • Stéphane Gimenez
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


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.


Linear Logic Proof Nets Differential Linear Logic Differential Interaction Nets Realizability Weak Normalization 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ehrhard, T., Regnier, L.: The differential lambda-calculus. In: TCS, vol. 309, pp. 1–41. Elsevier Science Publishers Ltd., Amsterdam (2004)Google Scholar
  2. 2.
    Ehrhard, T., Regnier, L.: Differential interaction nets. In: TCS, vol. 364, pp. 166–195. Elsevier Science Publishers Ltd., Amsterdam (2006)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)CrossRefzbMATHGoogle Scholar
  5. 5.
    Lafont, Y.: Interaction nets. In: Principles of Programming Languages, pp. 95–108. ACM, New York (1990)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Pagani, M., de Falco, L.T.: Strong Normalization Property for Second Order Linear Logic. Theoretical Computer Science 411(2), 410–444 (2010)CrossRefzbMATHGoogle Scholar
  9. 9.
    Tranquilli, P.: Intuitionistic differential nets and lambda-calculus. Theoretical Computer Science 412(20), 1979–1997 (2011)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Stéphane Gimenez
    • 1
  1. 1.Laboratoire PPSUniversité Paris-DiderotParis 7France

Personalised recommendations