Skip to Main content Skip to Navigation
Conference papers

The Prismoid of Resources

Abstract : 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 as a particular case of the general abstract proofs.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/inria-00519503
Contributor : Delia Kesner <>
Submitted on : Monday, September 20, 2010 - 5:44:12 PM
Last modification on : Friday, March 27, 2020 - 4:00:18 AM
Long-term archiving on: : Tuesday, October 23, 2012 - 4:22:00 PM

File

submission-mfcs-19-04-2009.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00519503, version 1

Collections

Citation

Delia Kesner, Fabien Renaud. The Prismoid of Resources. Mathematical Foundations of Computer Science, Aug 2010, Novy Smokovec, Slovakia. pp.464-476. ⟨inria-00519503⟩

Share

Metrics

Record views

238

Files downloads

203