Verifying Selective CPS Transformation for Shift and Reset

DOI10.1007/978-3-030-47147-7_3zbMath1503.68037OpenAlexW3022311398MaRDI QIDQ5098734

Kenichi Asai, Chiaki Ishio

Publication date: 30 August 2022

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-47147-7_3

zbMATH Keywords

shiftresetAgdaPHOASselective CPS transformation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (1)

A Functional Abstraction of Typed Invocation Contexts

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
• Mechanized Verification of CPS Transformations
• Representing Control: a Study of the CPS Transformation
• Subtyping delimited continuations
• Parametric higher-order abstract syntax for mechanized semantics
• A sound and complete axiomatization of delimited continuations
• Certifying CPS transformation of let-polymorphic calculus using PHOAS

This page was built for publication: Verifying Selective CPS Transformation for Shift and Reset