The Prismoid of Resources

13 years 10 months ago
The Prismoid of Resources
We define a framework called the prismoid of resources where each vertex refines the λ-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of β-reduction, confluence, preservation of β-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained ticular case of the general abstract proofs.
Delia Kesner, Fabien Renaud
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where MFCS
Authors Delia Kesner, Fabien Renaud
Comments (0)