Abstract : We investigate the control of evaluation strategies in a variant of the λ-calculus derived through the Curry-Howard correspondence from LJF, a sequent calculus for intuitionistic logic implementing the focusing technique. The proof theory of focused intuitionistic logic yields a single calculus in which a number of known λ-calculi appear as subsystems obtained by restricting types to a certain fragment of LJF. In particular, standard λ-calculi as well as the call-by-push-value calculus are analysed using this framework, and we relate cut elimination for LJF to a new abstract machine subsuming well-known machines for these different strategies.
https://hal.inria.fr/hal-01249216
Contributeur : Taus Brock-Nannestad
<>
Soumis le : mercredi 30 décembre 2015 - 16:53:36
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : mardi 5 avril 2016 - 13:47:44
