On Inter-deriving Small-step and Big-step Semantics: A Case Study for Storeless Call-by-need Evaluation

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Standard

On Inter-deriving Small-step and Big-step Semantics : A Case Study for Storeless Call-by-need Evaluation. / Danvy, Olivier; Millikin, Kevin; Munk, Johan; Zerny, Ian.

In: Theoretical Computer Science, Vol. 435, 2012, p. 21–42.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Harvard

APA

CBE

MLA

Vancouver

Author

Danvy, Olivier ; Millikin, Kevin ; Munk, Johan ; Zerny, Ian. / On Inter-deriving Small-step and Big-step Semantics : A Case Study for Storeless Call-by-need Evaluation. In: Theoretical Computer Science. 2012 ; Vol. 435. pp. 21–42.

Bibtex

@article{744c387278e04b1fbec563504dad078a,
title = "On Inter-deriving Small-step and Big-step Semantics: A Case Study for Storeless Call-by-need Evaluation",
abstract = "Starting from the standard call-by-need reduction for the λ-calculus that is common to Ariola, Felleisen, Maraist, Odersky, and Wadler, we inter-derive a series of hygienic semantic artifacts: a reduction-free storeless abstract machine, a continuation-passing evaluation function, and what appears to be the first heapless natural semantics for call-by-need evaluation. Furthermore we observe that the evaluation function implementing this natural semantics is in defunctionalized form. The refunctionalized counterpart of this evaluation function implements an extended direct semantics in the sense of Cartwright and Felleisen.Overall, the semantic artifacts presented here are simpler than many other such artifacts that have been independently worked out, and which require ingenuity, skill, and independent soundness proofs on a case-by-case basis. They are also simpler to inter-derive because the inter-derivational tools (e.g., refocusing and defunctionalization) already exist.",
author = "Olivier Danvy and Kevin Millikin and Johan Munk and Ian Zerny",
year = "2012",
doi = "10.1016/j.tcs.2012.02.023",
language = "English",
volume = "435",
pages = "21–42",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier BV",

}

RIS

TY - JOUR

T1 - On Inter-deriving Small-step and Big-step Semantics

T2 - A Case Study for Storeless Call-by-need Evaluation

AU - Danvy, Olivier

AU - Millikin, Kevin

AU - Munk, Johan

AU - Zerny, Ian

PY - 2012

Y1 - 2012

N2 - Starting from the standard call-by-need reduction for the λ-calculus that is common to Ariola, Felleisen, Maraist, Odersky, and Wadler, we inter-derive a series of hygienic semantic artifacts: a reduction-free storeless abstract machine, a continuation-passing evaluation function, and what appears to be the first heapless natural semantics for call-by-need evaluation. Furthermore we observe that the evaluation function implementing this natural semantics is in defunctionalized form. The refunctionalized counterpart of this evaluation function implements an extended direct semantics in the sense of Cartwright and Felleisen.Overall, the semantic artifacts presented here are simpler than many other such artifacts that have been independently worked out, and which require ingenuity, skill, and independent soundness proofs on a case-by-case basis. They are also simpler to inter-derive because the inter-derivational tools (e.g., refocusing and defunctionalization) already exist.

AB - Starting from the standard call-by-need reduction for the λ-calculus that is common to Ariola, Felleisen, Maraist, Odersky, and Wadler, we inter-derive a series of hygienic semantic artifacts: a reduction-free storeless abstract machine, a continuation-passing evaluation function, and what appears to be the first heapless natural semantics for call-by-need evaluation. Furthermore we observe that the evaluation function implementing this natural semantics is in defunctionalized form. The refunctionalized counterpart of this evaluation function implements an extended direct semantics in the sense of Cartwright and Felleisen.Overall, the semantic artifacts presented here are simpler than many other such artifacts that have been independently worked out, and which require ingenuity, skill, and independent soundness proofs on a case-by-case basis. They are also simpler to inter-derive because the inter-derivational tools (e.g., refocusing and defunctionalization) already exist.

U2 - 10.1016/j.tcs.2012.02.023

DO - 10.1016/j.tcs.2012.02.023

M3 - Journal article

VL - 435

SP - 21

EP - 42

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -