Verifying selective CPS transformation for shift and reset

DOI10.1007/978-3-030-47147-7_3MaRDI QIDQ5098734zbMATH OpenOpenAlexFDO

Authors Chiaki Ishio, Kenichi Asai

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

AgdaPHOASresetselective CPS transformationshift

Mathematics Subject Classification ID

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

Recommendations

• A selective CPS transformation
• Mechanized Verification of CPS Transformations
• Certifying CPS transformation of let-polymorphic calculus using PHOAS
• A static simulation of dynamic delimited control
• Representing Control: a Study of the CPS Transformation

Cites work

• A sound and complete axiomatization of delimited continuations
• Certifying CPS transformation of let-polymorphic calculus using PHOAS
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
• Logical relations for coherence of effect subtyping
• Mechanized Verification of CPS Transformations
• Parametric higher-order abstract syntax for mechanized semantics
• Representing Control: a Study of the CPS Transformation
• Subtyping delimited continuations

Cited in

(3)

• A selective CPS transformation
• A Functional Abstraction of Typed Invocation Contexts
• Certifying CPS transformation of let-polymorphic calculus using PHOAS

This page was built for publication: Verifying selective CPS transformation for shift and reset

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5098734)