Explicit substitutions
- 1 October 1991
- journal article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 1 (4) , 375-416
- https://doi.org/10.1017/s0956796800000186
Abstract
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.Keywords
This publication has 5 references indexed in Scilit:
- Strong normalization of substitutionsPublished by Springer Nature ,1992
- Confluence results for the pure strong categorical logic CCL. λ-calculi as subsystems of CCLTheoretical Computer Science, 1989
- Proof of termination of the rewriting system subst on CCLTheoretical Computer Science, 1986
- Equations and Rewrite Rules: A SurveyPublished by Elsevier ,1980
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972