Explicit substitutions. (English) Zbl 0941.68542

Summary: The \(\lambda\sigma\)-calculus is a refinement of the \(\lambda\)-calculus where substitutions are manipulated explicitly. The \(\lambda\sigma\)-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical \(\lambda\)-calculus and concrete implementations.


68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing
03B40 Combinatory logic and lambda calculus
Full Text: DOI


[1] Curry, Combinatory Logic 1 (1958)
[2] Klop, Combinatory Reduction Systems (1980) · Zbl 0466.03006
[3] Curien, Categorical Combinators, Sequential Algorithms and Functional Programming (1986)
[4] DOI: 10.1016/0304-3975(89)90105-9 · Zbl 0707.03012
[5] De Bruijn, Indag. Mat. 34 pp 381– (1972)
[6] DOI: 10.1016/0304-3975(86)90035-6 · Zbl 0618.68031
[7] Barendregt, The Lambda Calculus: Its Syntax and Semantics (1985) · Zbl 0597.03009
[8] Huet, Formal Languages Theory: Perspectives and Open Problems pp 349– (1980)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.