Mechanized Verification of CPS Transformations

DOI10.1007/978-3-540-75560-9_17MaRDI QIDQ3498467zbMATH OpenOpenAlexFDO

Authors Zaynah Dargaye, Xavier Leroy

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75560-9_17

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• A first-order one-pass CPS transformation
• scientific article; zbMATH DE number 2087425
• Representing Control: a Study of the CPS Transformation
• scientific article; zbMATH DE number 1497779
• CPS transformation of beta-redexes

Cites work

• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A first-order one-pass CPS transformation
• CPS transformation of beta-redexes
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Compiling with continuations, continued
• Explicit substitutions
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Nominal techniques in Isabelle/HOL
• Programming Languages and Systems
• Theorem Proving in Higher Order Logics

Cited in

(4)

• Verifying selective CPS transformation for shift and reset
• Certifying CPS transformation of let-polymorphic calculus using PHOAS
• Formal Methods in Computer-Aided Design
• A verified runtime for a verified theorem prover

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Mechanized Verification of CPS Transformations

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