Name
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1145/2790449.2790528 | PPDP |
Keywords | Field | DocType |
Intuitionistic Logic, Curry-Howard, Lambda-calculus, Focusing, Polarities, Evaluation Strategies, Abstract Machines | Intuitionistic logic,Computer science,Natural deduction,Proof calculus,Minimal logic,Algorithm,Theoretical computer science,Many-valued logic,Cut-elimination theorem,Dependent type,Calculus,Curry–Howard correspondence | Conference |
Citations | PageRank | References |
1 | 0.36 | 23 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Taus Brock-Nannestad | 1 | 15 | 4.10 |
| Nicolas Guenot | 2 | 1 | 1.71 |
| Daniel Gustafsson | 3 | 1 | 0.36 |