A syntactic correspondence between context-sensitive calculi and abstract machines
From MaRDI portal
Publication:879356
DOI10.1016/j.tcs.2006.12.028zbMath1111.68065OpenAlexW1981224255MaRDI QIDQ879356
Olivier Danvy, Małgorzata Biernacka
Publication date: 11 May 2007
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.028
contextsreduction semanticsexplicit substitutionscontinuationsrefocusingdefunctionalizationdelimited continuationsenvironment-based machinesproper tail recursionstack inspection
Formal languages and automata (68Q45) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)
Related Items
From Outermost Reduction Semantics to Abstract Machine ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ Inter-deriving Semantic Artifacts for Object-Oriented Programming ⋮ On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation ⋮ Refunctionalization at work ⋮ A call-by-name lambda-calculus machine ⋮ A static simulation of dynamic delimited control ⋮ On graph rewriting, reduction, and evaluation in the presence of cycles ⋮ On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion ⋮ On one-pass CPS transformations ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ Unnamed Item ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ Unnamed Item ⋮ From Reduction-Based to Reduction-Free Normalization
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- An abstract framework for environment machines
- A syntactic correspondence between context-sensitive calculi and abstract machines
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- A syntactic theory of dynamic binding
- An introduction to Landin's ``A generalization of jumps and labels
- A generalization of jumps and labels
- Definitional interpreters revisited
- Definitional interpreters for higher-order programming languages
- The first report on scheme revisited
- Scheme: A interpreter for extended lambda calculus
- Implementation strategies for first-class continuations
- An early use of continuations and partial evaluation for compiling rules written in first-order predicate calculus
- Fundamental concepts in programming languages
- Continuations revisited
- Continuations: A mathematical semantics for handling full jumps
- A functional correspondence between call-by-need evaluators and lazy abstract machines
- On the static and dynamic extents of delimited continuations
- A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
- Trampolined style
- Recursive functions of symbolic expressions and their computation by machine, Part I
- A Rational Deconstruction of Landin’s J Operator
- An environment machine for the λμ-calculus
- Functional runtime systems within the lambda-sigma calculus
- Representing Control: a Study of the CPS Transformation
- Deriving a lazy abstract machine
- Confluence properties of weak and strong calculi of explicit substitutions
- Explicit substitutions
- Making a fast curry
- An Operational Foundation for Delimited Continuations in the CPS Hierarchy
- Computer Science Logic
- A Rational Deconstruction of Landin’s SECD Machine
- THEORETICAL PEARL: A simple proof of a folklore theorem about delimited control
- Logic Based Program Synthesis and Transformation
- The Mechanical Evaluation of Expressions
