Mechanized Verification of CPS Transformations
From MaRDI portal
Publication:3498467
DOI10.1007/978-3-540-75560-9_17zbMath1137.68345MaRDI QIDQ3498467
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
68N18: Functional programming and lambda calculus
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- 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
- CPS transformation of beta-redexes
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- A first-order one-pass CPS transformation
- Explicit substitutions
- Compiling with continuations, continued
- Formal certification of a compiler back-end or
- Theorem Proving in Higher Order Logics
- Programming Languages and Systems