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
1 Department of Computer and Information Science
2 PPS - Preuves, Programmes et Systèmes
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
4 Institute of Cybernetics [Tallinn]
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.
Keywords : call-by-need lazy evaluation duality of computation sequent calculus lambda-mu-calculus classical logic control
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 : mardi 17 avril 2018 - 11:26:42
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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

205

Téléchargements de fichiers

100

Contact


archive-ouverte@inria.fr