Representing Control: a Study of the CPS Transformation

DOI10.1017/S0960129500001535zbMath0798.68102OpenAlexW1999336811WikidataQ56430282 ScholiaQ56430282MaRDI QIDQ4279251

Andrzej Filinski, Olivier Danvy

Publication date: 31 October 1994

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129500001535

zbMATH Keywords

continuation-passing styleequational specificationCPS transformation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items (33)

A first-order one-pass CPS transformation ⋮ Probabilistic operational semantics for the lambda calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the relations between monadic semantics ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ Verifying Selective CPS Transformation for Shift and Reset ⋮ Effect handlers via generalised continuations ⋮ Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala ⋮ Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus ⋮ UTP Semantics of Reactive Processes with Continuations ⋮ On the semantics of parsing actions ⋮ Delimited control operators prove double-negation shift ⋮ Refunctionalization at work ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ Type checking and typability in domain-free lambda calculi ⋮ Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence ⋮ Programming with algebraic effects and handlers ⋮ A New Method for Dependent Parsing ⋮ A Selective CPS Transformation ⋮ A New Criterion for Safe Program Transformations ⋮ Unnamed Item ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ Unnamed Item ⋮ From Reduction-Based to Reduction-Free Normalization ⋮ A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell* ⋮ Syntactic Theories in Practice ⋮ CPS transformation of beta-redexes ⋮ Continuation passing style for effect handlers ⋮ A functional correspondence between monadic evaluators and abstract machines for languages with computational effects ⋮ Type-Safe Code Transformations in Haskell

Cites Work

• Two-level semantics and abstract interpretation
• Two-level semantics and code generation
• A syntactic theory of sequential control
• Automatic autoprojection of recursive equations with global variables and abstract data types
• Automatic autoprojection of higher order recursive equations
• Call-by-name, call-by-value and the \(\lambda\)-calculus

This page was built for publication: Representing Control: a Study of the CPS Transformation