Proof Pearl: Abella Formalization of λ-Calculus Cube Property
No abstract available.
DOI 10.1007/978-3-642-35308-6_15
Related papers
- A Lightweight Formalization of the Metatheory of Bisimulation-Up-To CPP 2015
- Modular Proof of Strong Normalization for the Calculus of Constructions JFP 1991
- Separation logic for sequential programs (functional pearl) ICFP 2020
- Residual Theory in lambda-Calculus: A Formal Development JFP 1994
- Functional pearl: streams and unique fixed points ICFP 2008
- No-brainer CPS conversion (functional pearl) ICFP 2017
- An Equational and Graphical Fixed-Point Calculus (Functional Pearl) ICFP 2026
- Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl) ICFP 2026