| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Computation in Focused Intuitionistic Logic
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.
Cited literature [29 references]
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
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