The Prismoid of Resources - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

The Prismoid of Resources

Delia Kesner
  • Fonction : Auteur
  • PersonId : 836418
Fabien Renaud
  • Fonction : Auteur
  • PersonId : 879413

Résumé

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.
Fichier principal
Vignette du fichier
submission-mfcs-19-04-2009.pdf (206.81 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00519503 , version 1 (20-09-2010)

Identifiants

  • HAL Id : inria-00519503 , version 1

Citer

Delia Kesner, Fabien Renaud. The Prismoid of Resources. Mathematical Foundations of Computer Science, Aug 2010, Novy Smokovec, Slovakia. pp.464-476. ⟨inria-00519503⟩
136 Consultations
78 Téléchargements

Partager

Gmail Facebook X LinkedIn More