Name
Abstract | ||
|---|---|---|
We propose a sequent calculus derived from the λ―μμ˜-calculus of Curien and Herbelin that is expressive enough to directly represent the fine details of program evaluation using typical abstract machines. Not only does the calculus easily encode the usual components of abstract machines such as environments and stacks, but it can also simulate the transition steps of the abstract machine with just a constant overhead. Technically this is achieved by ensuring that reduction in the calculus always happens at a bounded depth from the root of the term. We illustrate these properties by providing shallow encodings of the Krivine (call-by-name) and the CEK (call-by-value) abstract machines in the calculus. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1145/1516507.1516508 | ACM Trans. Program. Lang. Syst. |
Keywords | Field | DocType |
typical abstract machine,transition step,curry-howard isomorphism,duality,abstract machine,explicit substitutions,bounded depth,fine detail,program evaluation,sequent calculus,usual component,constant overhead,krivine machine,shallow encodings,natural deduction,curry howard isomorphism | Lambda calculus,Operational semantics,Programming language,Natural deduction,Computer science,Sequent calculus,Sequent,Process calculus,Abstract machine,Curry–Howard correspondence | Journal |
Volume | Issue | ISSN |
31 | 4 | 0164-0925 |
Citations | PageRank | References |
10 | 0.59 | 31 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Zena M. Ariola | 1 | 482 | 38.61 |
| Aaron Bohannon | 2 | 296 | 12.72 |
| Amr Sabry | 3 | 520 | 35.46 |