A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
From MaRDI portal
Publication:1945915
DOI10.1007/s10817-011-9231-4zbMath1260.68366OpenAlexW2077540255MaRDI QIDQ1945915
Publication date: 17 April 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9231-4
Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- More Church-Rosser proofs (in Isabelle/HOL)
- Isabelle/HOL. A proof assistant for higher-order logic
- Turning Inductive into Equational Specifications
- Residual theory in λ-calculus: a formal development
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- Types for Proofs and Programs