Computation in Focused Intuitionistic Logic

Taus Brock-Nannestad 1, * Nicolas Guenot 2 Daniel Gustafsson 2
* Auteur correspondant
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
17th International Symposium on Principles and Practice of Declarative Programming, Jul 2015, Siena, Italy. 2015, 〈http://costa.ls.fi.upm.es/ppdp15/〉. 〈10.1145/2790449.2790528〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01249216
Contributeur : Taus Brock-Nannestad <>
Soumis le : mercredi 30 décembre 2015 - 16:53:36
Dernière modification le : jeudi 10 mai 2018 - 02:06:27
Document(s) archivé(s) le : mardi 5 avril 2016 - 13:47:44

Fichier

ppdp15computation.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Citation

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. 2015, 〈http://costa.ls.fi.upm.es/ppdp15/〉. 〈10.1145/2790449.2790528〉. 〈hal-01249216〉

Partager

Métriques

Consultations de la notice

358

Téléchargements de fichiers

106