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
Document type :
Conference papers
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download
https://hal.inria.fr/hal-00697241
Contributor : Hugo Herbelin <>
Submitted on : Tuesday, May 15, 2012 - 3:56:03 AM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM
Long-term archiving on : Friday, November 30, 2012 - 11:41:23 AM

File

classical-need-artifacts.pdf
Files produced by the author(s)

Identifiers

Collections

UNIV-PARIS7 | INRIA | PPS | USPC | INRIA-ROCQ

Citation

Zena Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin. Classical call-by-need sequent calculi : The unity of semantic artifacts. FLOPS 2012 - 11th International Symposium on Functional and Logic Programming, May 2012, Kobe, Japan. pp.32-46, ⟨10.1007/978-3-642-29822-6⟩. ⟨hal-00697241⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

255

Files downloads

159

Contact


archive-ouverte@inria.fr