A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines Export

@techreport{citeulike:915727, abstract = {We present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with ten calculi and machines for applicative order with an abort operation, normal order with generalized reduction and call/cc, the lambda-mu-calculus, delimited continuations, 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.}, author = {Biernacka, Ma{\l}gorzata and Danvy, Olivier}, citeulike-article-id = {915727}, citeulike-linkout-0 = {http://www.brics.dk/RS/05/38/index.html}, institution = {BRICS}, keywords = {abstract-machine, contexts, continuation-marks, continuations, control, control-operators, cps, defunctionalization, return, tail-recursion}, month = {December}, posted-at = {2006-10-28 10:21:32}, priority = {2}, title = {A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines}, url = {http://www.brics.dk/RS/05/38/index.html}, year = {2005} }

TY - RPRT ID - citeulike:915727 L3 - citeulike-article-id:915727 N2 - We present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with ten calculi and machines for applicative order with an abort operation, normal order with generalized reduction and call/cc, the lambda-mu-calculus, delimited continuations, 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. TI - A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines KW - abstract-machine KW - contexts KW - continuation-marks KW - continuations KW - control KW - control-operators KW - cps KW - defunctionalization KW - return KW - tail-recursion AU - Biernacka, Małgorzata AU - Danvy, Olivier PY - 2005/12// UR - http://www.brics.dk/RS/05/38/index.html ER -