Certifying CPS transformation of let-polymorphic calculus using PHOAS

DOI10.1007/978-3-030-02768-1_20MaRDI QIDQ6166157zbMATH OpenOpenAlexFDO

Authors Urara Yamada, Kenichi Asai

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-02768-1_20

zbMATH Keywords

Agdaone-pass CPS transformationlet-polymorphismparameterized higher-order abstract syntax

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Mechanized Verification of CPS Transformations
• A first-order one-pass CPS transformation
• Verifying selective CPS transformation for shift and reset
• Representing Control: a Study of the CPS Transformation
• Parametric higher-order abstract syntax for mechanized semantics

Cited in

(1)

• Verifying selective CPS transformation for shift and reset

This page was built for publication: Certifying CPS transformation of let-polymorphic calculus using PHOAS

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