Classical call-by-need sequent calculi : The unity of semantic artifacts

Zena Ariola 1 Paul Downen 1 Hugo Herbelin 2, 3 Keiko Nakata 4 Alexis Saurin 2, 3
3 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We systematically derive a classical call-by-need sequent calculus, which does not require an unbounded search for the standard redex, by using the unity of semantic artifacts proposed by Danvy et al. The calculus serves as an intermediate step toward the generation of an environment-based abstract machine. The resulting abstract machine is context-free, so that each step is parametric in all but one component. The context-free machine elegantly leads to an environment-based CPS transformation. This transformation is observationally different from a natural classical extension of the transformation of Okasaki et al., due to duplication of un-evaluated bindings.
Type de document :
Communication dans un congrès
Tom Schrijvers and Peter Thiemann. FLOPS 2012 - 11th International Symposium on Functional and Logic Programming, May 2012, Kobe, Japan. Springer, 7294, pp.32-46, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-29822-6〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00697241
Contributeur : Hugo Herbelin <>
Soumis le : mardi 15 mai 2012 - 03:56:03
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : vendredi 30 novembre 2012 - 11:41:23

Fichier

classical-need-artifacts.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | PPS | USPC

Citation

Zena Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin. Classical call-by-need sequent calculi : The unity of semantic artifacts. Tom Schrijvers and Peter Thiemann. FLOPS 2012 - 11th International Symposium on Functional and Logic Programming, May 2012, Kobe, Japan. Springer, 7294, pp.32-46, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-29822-6〉. 〈hal-00697241〉

Partager

Métriques

Consultations de la notice

217

Téléchargements de fichiers

105