Record Details

A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines

BRICS Report Series

View Archive Info
 
 
Field Value
 
Title A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines
 
Creator Biernacka, Malgorzata
Danvy, Olivier
 
Description We present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with a series of calculi and machines: Krivine's machine with call/cc, the lambda-mu-calculus, delimited continuations, i/o, stack inspection, proper tail-recursion, and lazy evaluation. Most of the machines already exist but have been obtained independently and are only indirectly related to the corresponding calculi. All of the calculi are new and they make it possible to directly reason about the execution of the corresponding machines. In connection with the functional correspondence between evaluation functions and abstract machines initiated by Reynolds, the present syntactic correspondence makes it possible to construct reduction-free normalization functions out of reduction-based ones, which was an open problem in the area of normalization by evaluation.
 
Publisher Aarhus University
 
Contributor —
 
Date 2005-07-11
 
Type info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
—
 
Format application/pdf
 
Identifier https://tidsskrift.dk/brics/article/view/21888
10.7146/brics.v12i22.21888
 
Source BRICS Report Series; No 22 (2005): RS-22 A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines
BRICS Report Series; No 22 (2005): RS-22 A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines
1601-5355
0909-0878
 
Language eng
 
Relation https://tidsskrift.dk/brics/article/view/21888/19315
 
Rights Copyright (c) 2015 BRICS Report Series