Explicit substitutions

ABSTRACT

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

REFERENCES

• 1: tt.P. Barendregt, The Lambda Calculus" Its Syntax and Semantic,s, North Holland, 1985.
• 2: N. De Bruijn, Lambda-calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, Indag. Mat. 34, pp. 381-392, 1972.
• 3: L. Cardelli, Typeful Programming, SRC Report No. 45, Digital Equipment Corporation, 1989.
• 4: H.P. Curry and R. Feys, Combinatory Logic, Vol. 1, North Holland, 1958.
• 5: P.-L. Curien, The Ap-calculi: An Abstract Framework for Closures, unpublished (preliminary version printed as LIENS report, 1988).
• 6: Pierre-Louis Curien, Categorical combinators, sequential algorithms, and functional programming (2nd ed.), Birkhauser Boston Inc., Cambridge, MA, 1994
• 7: T. Ilardin, Confluence Results for the Pure Strong Categorical Combinatory Logic, to appear in Theoretical Computer Science, 1988.
• 8: T Hardin , A Laville, Proof of termination of the rewriting system SUBST on CCL, Theoretical Computer Science, v.46 n.2-3, p.305-312, Oct. 1986
• 9: G. Huet, D.C. Oppen, Equations and Rewrite Rules: A Survey, in Formal Languages Theory: Perspectives and Open Problems (R. Book, editor), pp. 349-393, Academic Press, 1980.
• 10: J.W. Klop, Combinatory Reduction Systems, Math. Center Tracts 129, Amsterdam, 1980.
• 11: J.-L. Krivine, unpublished.
• 12: P. Martin-LSf, Intuitionislic Type Theory, notes by G. Sambin of a series of lectures given in Padova in 1980, Bibliopolis, 1984.
• 13: C.P, Wadsworth, Semantics and Pragmatics of the Lambda Calculus, Dissertation, Oxford University, 1971.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Algorithms, Languages, Theory