Skip to Main content Skip to Navigation
Conference papers

Computation in Focused Intuitionistic Logic

Taus Brock-Nannestad 1, * Nicolas Guenot 2 Daniel Gustafsson 2
* Corresponding author
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01249216
Contributor : Taus Brock-Nannestad <>
Submitted on : Wednesday, December 30, 2015 - 4:53:36 PM
Last modification on : Friday, April 30, 2021 - 10:04:55 AM
Long-term archiving on: : Tuesday, April 5, 2016 - 1:47:44 PM

File

ppdp15computation.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License

Identifiers

Collections

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. ⟨10.1145/2790449.2790528⟩. ⟨hal-01249216⟩

Share

Metrics

Record views

819

Files downloads

543