Proof Pearl: Abella Formalization of λ-Calculus Cube Property
From MaRDI portal
Publication:4916060
DOI10.1007/978-3-642-35308-6_15zbMath1385.68012OpenAlexW2110359479MaRDI QIDQ4916060
Publication date: 19 April 2013
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-35308-6_15
Related Items (3)
The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ Mechanized metatheory revisited
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Nominal abstraction
- The lambda calculus. Its syntax and semantics. Rev. ed.
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- Relating conflict-free stable transition and event models via redex families
- A two-level logic approach to reasoning about computations
- On the Expressivity of Minimal Generic Quantification
- Reasoning in Abella about Structural Operational Semantics Specifications
- Proof search specifications of bisimulation and modal logics for the π-calculus
- The Abella Interactive Theorem Prover (System Description)
- A mechanical proof of the Church-Rosser theorem
- More Church-Rosser proofs (in Isabelle/HOL)
- Residual theory in λ-calculus: a formal development
- A proof theory for generic judgments
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Parallel reductions in \(\lambda\)-calculus
This page was built for publication: Proof Pearl: Abella Formalization of λ-Calculus Cube Property
