Since 2014
A Concrete Framework for Environment Machines
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
A Concrete Framework for Environment Machines
|
|
| Creator |
Biernacka, Malgorzata
Danvy, Olivier |
|
| Description |
We materialize the common belief that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to Curien's original calculus of closures (an early calculus with explicit substitutions), we extend it minimally so that it can express one-step reduction strategies, and we methodically derive a series of environment machines from the specification of two one-step reduction strategies for the lambda-calculus: normal order and applicative order. The derivation extends Danvy and Nielsen's refocusing-based construction of abstract machines with two new steps: one for coalescing two successive transitions into one, and one for unfolding a closure into a term and an environment in the resulting abstract machine. The resulting environment machines include both the idealized and the original versions of Krivine's machine, Felleisen et al.'s CEK machine, and Leroy's Zinc abstract machine.
|
|
| Publisher |
Aarhus University
|
|
| Contributor |
—
|
|
| Date |
2005-05-11
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion — |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/21881
10.7146/brics.v12i15.21881 |
|
| Source |
BRICS Report Series; No 15 (2005): RS-15 A Concrete Framework for Environment Machines
BRICS Report Series; No 15 (2005): RS-15 A Concrete Framework for Environment Machines 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/21881/19308
|
|
| Rights |
Copyright (c) 2015 BRICS Report Series
|
|