Abstract
We derive an abstract machine from the Curry-Howard correspondence with a sequent calculus presentation of Intuitionistic Propositional Linear Logic. The states of the register based abstract machine comprise a low-level code block, a register bank and a dump holding suspended procedure activations. Transformation of natural deduction proofs into our sequent calculus yields a type-preserving compilation function from the Linear Lambda Calculus to the abstract machine. We prove correctness of the abstract machine with respect to the standard call-by-value evaluation semantics of the Linear Lambda Calculus.
| Original language | English |
|---|---|
| Pages (from-to) | 99-121 |
| Number of pages | 23 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 158 |
| Issue number | 1 |
| DOIs | |
| State | Published - 5 May 2006 |
Keywords
- Abstract Machine
- Compilation
- Curry-Howard Isomorphism
- Linear Lambda Calculus
- Linear Logic
Fingerprint
Dive into the research topics of 'The Linear Logical Abstract Machine'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver