| |
SPECIAL ISSUE:
(in progress)
|
A Theory of Explicit Substitutions with Safe and Full Composition
|
©Delia Kesner, PPS, Universite Paris-Diderot and CNRS
|
Abstract
Many different systems with explicit substitutions have been proposed to
implement a large class of higher-order languages. Motivations and challenges
that guided the development of such calculi in functional frameworks are
surveyed in the first part of this paper. Then, very simple technology in named
variable-style notation is used to establish a theory of explicit substitutions
for the lambda-calculus which enjoys a whole set of useful properties such as
full composition, simulation of one-step beta-reduction, preservation of
beta-strong normalisation, strong normalisation of typed terms and confluence
on metaterms. Normalisation of related calculi is also discussed.
|
Publication date: July 15, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(3:1)2009
Hit Counts: 3154 |
 Creative Commons | |
