Hostname: page-component-f554764f5-8cg97 Total loading time: 0 Render date: 2025-04-16T05:48:39.265Z Has data issue: false hasContentIssue false
  • English
  • Français

Explicit substitutions

Part of: JFP Research Articles

Published online by Cambridge University Press:  07 November 2008

M. Abadi ,
L. Cardelli ,
P.-L. Curien  and
J.-J. Lévy
M. Abadi
Affiliation:
Digital Equipment Corp., Systems Research Center, 130 Lytton Avenue, Palo Alto, California, USA94301
L. Cardelli
Affiliation:
Digital Equipment Corp., Systems Research Center, 130 Lytton Avenue, Palo Alto, California, USA94301
P.-L. Curien
Affiliation:
Laboratoire d'Informatique, Ecole Normale Supérieure, 45 Rue d'Ulm 75005, Paris, France
J.-J. Lévy
Affiliation:
INRIA, Domaine de Voluceau, Rocquencourt, B.P. 105, 78153, Le Chesnay, Cedex, France
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The λσ-calculus is a refinement of the λ-calculus where substitutions are manipulated explicitly. The λσ-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical λ-calculus and concrete implementations.

Type
Articles
Information
Journal of Functional Programming , Volume 1 , Issue 4 , October 1991 , pp. 375 - 416
Copyright
Copyright © Cambridge University Press 1991

References

Barendregt, H. P. 1985. The Lambda Calculus: Its Syntax and Semantics. North Holland.Google Scholar
De Bruijn, N. 1972. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Mat. 34: 381–92.CrossRefGoogle Scholar
Cardelli, L. 1989. Typeful Programming, SRC Report No. 45. Digital Equipment Corporation.Google Scholar
Curien, P.-L. 1986. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman.Google Scholar
Curien, P.-L. 1988. The λπ-calculi: an Abstract Framework for Closures, unpublished (preliminary version printed as LIENS report).Google Scholar
Curien, P.-L., Hardin, T. and Lévy, J.-J. 1991 a. Confluence properties of weak and strong calculi of explicit substitutions (draft).Google Scholar
Curien, P.-L., Hardin, T. and Ríos, A. 1991 b. Normalisation forte des substitutions (draft).Google Scholar
Curien, P.-L. and Ríos, A. 1991. Un Résultat de Complétude pour les Substitutions Explicites.Google Scholar
Comptes Rendus de l'Académie des Sciences de Paris, t. 312, Série I, pp. 471–76.Google Scholar
Curry, H. P. and Feys, R. 1958. Combinatory Logic, vol. 1. North Holland.Google Scholar
Field, J. 1990. On laziness and optimality in lambda interpreters: tools for specification and analysis. In 17th Annual ACM Symposium on Principles of Programming Languages,San Francisco, USA,january, pp. 1–15.Google Scholar
Hardin, T. 1989. Confluence results for the pure strong categorical combinatory logic CCL: λ-calculi as subsystems of CCL, Theor. Comput. Sci. 65: 291–342.CrossRefGoogle Scholar
Hardin, T. and Laville, A. 1986. Proof of termination of rewriting system SUBST on CCL. Theor. Comput. Sci. 46: 305–12.CrossRefGoogle Scholar
Hardin, T. and Lévy, J.-J. 1989. A confluent calculus of substitutions. In France–Japan Artificial Intelligence and Computer Science Symposium,Izu, Japan,December.Google Scholar
Huet, G. and Oppen, D. C. 1980. Equations and rewrite rules: a survey. In Book, R. (editor), Formal Languages Theory: Perspectives and Open Problems, pp. 349–93. Academic Press.CrossRefGoogle Scholar
Klop, J. W. 1980. Combinatory Reduction Systems. Mathematical Center Tracts 129, Amsterdam.Google Scholar
Martin-Löf, P. 1984. Intuitionistic Type Theory, notes by G. Sambin of a series of lectures given in Padova in 1980. Bibliopolis.Google Scholar
Wadsworth, C. P. 1971. Semantics and Pragmatics of the Lambda Calculus, Dissertation, Oxford University.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.