Proof Pearl: Abella Formalization of λ-Calculus Cube Property

DOI10.1007/978-3-642-35308-6_15zbMath1385.68012OpenAlexW2110359479MaRDI QIDQ4916060

Beniamino Accattoli

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

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

• Coq
• Beluga
• Isabelle/HOL
• Twelf
• Abella

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