Explicit substitutions
Authors:
- 1 April 1991
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 1 (4) , 375-416
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 6 references indexed in Scilit:
- Strong normalization of substitutionsLecture Notes in Computer Science, 1992
- On laziness and optimality in lambda interpreters: tools for specification and analysis1990
- 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 Survey1980
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972