Skip to main content
SpringerLink
Log in

Strong normalization of substitutions

  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1992 (MFCS 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 629))

Abstract

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

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit Substitutions. Journal of Functional Programming, to appear.

    Google Scholar 

  2. 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. 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. P.-L. Curien. Categorical Combinators, Sequential Algotithms and Computer Science. Pitman, 1986.

    Google Scholar 

  5. 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. T. Hardin and A. Laville. Proof of Termination of the Rewriting System SUBST on CCL. Theoretical Computer Science, 46, 1986.

    Google Scholar 

  7. M. Sleep. Issues for implementing lambda languages. Notes for Ustica Workshop, September 1985.

    Google Scholar 

  8. 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 

Download references

Author information

Authors and Affiliations

  1. CNRS and LIENS, France

    P. -L. Curien

  2. INRIA, Rocquencourt

    T. Hardin

  3. CNAM, France

    T. Hardin

  4. LIENS, 45, rue d'Ulm, 75230, Paris Cedex 05, France

    A. Ríos

Authors
  1. P. -L. Curien
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. T. Hardin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. A. Ríos
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ivan M. Havel Václav Koubek

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Curien, P.L., Hardin, T., Ríos, A. (1992). Strong normalization of substitutions. In: Havel, I.M., Koubek, V. (eds) Mathematical Foundations of Computer Science 1992. MFCS 1992. Lecture Notes in Computer Science, vol 629. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55808-X_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-55808-X_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55808-8

  • Online ISBN: 978-3-540-47291-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation