Strong normalization of substitutions

  • P. -L. Curien
  • T. Hardin
  • A. Ríos
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 629)


λσ-calculus is an extended λ-calculus where substitutions are handled explicity. We prove the strong normalization of its subcalculus σ which computes substitutions.


Normal Form Reduction Step Graph Grammar Strong Normalization Strict Interpretation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ACCL90]
    M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit Substitutions. Journal of Functional Programming, to appear.Google Scholar
  2. [CHL91]
    P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. 1991. Submitted.Google Scholar
  3. [CHR91]
    P.-L. Curien, T. Hardin, and A. Ríos. Normalisation Forte du Calcul des Substitutions. Technical Report, LIENS-Ecole Normale Supérieure, 1991.Google Scholar
  4. [Cur86]
    P.-L. Curien. Categorical Combinators, Sequential Algotithms and Computer Science. Pitman, 1986.Google Scholar
  5. [Har89]
    T. Hardin. Confluence Results for the Pure Strong Categorical Logic CCL: λ-calculi as Subsystems of CCL. Theoretical Computer Science, 65(2), 1989.Google Scholar
  6. [HL86]
    T. Hardin and A. Laville. Proof of Termination of the Rewriting System SUBST on CCL. Theoretical Computer Science, 46, 1986.Google Scholar
  7. [Sle85]
    M. Sleep. Issues for implementing lambda languages. Notes for Ustica Workshop, September 1985.Google Scholar
  8. [Sta78]
    J. Staples. A Graph-like Lambda-Calculus for which leftmost-outermost reduction is optimal. In Claus, editor, Graph Grammars and their Applications to Computer Science and Biology, Springer-Verlag, 1978.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • P. -L. Curien
    • 1
  • T. Hardin
    • 2
    • 3
  • A. Ríos
    • 4
  1. 1.CNRS and LIENSFrance
  2. 2.INRIARocquencourt
  3. 3.CNAMFrance
  4. 4.LIENSParis Cedex 05France

Personalised recommendations