A certified extension of the Krivine machine for a call-by-name higher-order imperative language
In this paper we present a compiler that translates programs from an imperative higher-order language into a sequence of instructions for an abstract machine. We consider an extension of the Krivine machine for the call-by-name lambda calculus, which includes strict operators and imperative features. We show that the compiler is correct with respect to the big-step semantics of our language, both for convergent and divergent programs.
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | article biblioteca |
| Language: | eng |
| Published: |
2014
|
| Subjects: | Abstract machines, Compiler correctness, Big-step semantics, Algol like language, Call by name, Krivine machine, |
| Online Access: | http://hdl.handle.net/11086/30119 http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.230 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|