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.
Type de document :
Communication dans un congrès
Mathematical Foundations of Computer Science, Aug 2010, Novy Smokovec, Slovakia. 5734, pp.464-476, 2009, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00519503
Contributeur : Delia Kesner <>
Soumis le : lundi 20 septembre 2010 - 17:44:12
Dernière modification le : jeudi 11 janvier 2018 - 06:17:47
Document(s) archivé(s) le : mardi 23 octobre 2012 - 16:22:00

Fichier

submission-mfcs-19-04-2009.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00519503, version 1

Collections

PPS | USPC

Citation

Delia Kesner, Fabien Renaud. The Prismoid of Resources. Mathematical Foundations of Computer Science, Aug 2010, Novy Smokovec, Slovakia. 5734, pp.464-476, 2009, Lecture Notes in Computer Science. 〈inria-00519503〉

Partager

Métriques

Consultations de la notice

144

Téléchargements de fichiers

73