Computation in Focused Intuitionistic Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Computation in Focused Intuitionistic Logic

Résumé

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

Dates et versions

hal-01249216 , version 1 (30-12-2015)

Licence

Paternité - Pas de modifications

Identifiants

Citer

Taus Brock-Nannestad, Nicolas Guenot, Daniel Gustafsson. Computation in Focused Intuitionistic Logic. 17th International Symposium on Principles and Practice of Declarative Programming, Jul 2015, Siena, Italy. ⟨10.1145/2790449.2790528⟩. ⟨hal-01249216⟩
612 Consultations
401 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More