A solution to the PoplMark challenge based on de Bruijn indices
From MaRDI portal
Publication:1945917
DOI10.1007/s10817-011-9230-5zbMath1260.68381OpenAlexW2006714020MaRDI QIDQ1945917
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-9230-5
Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Nominal techniques in Isabelle/HOL
- More Church-Rosser proofs (in Isabelle/HOL)
- Nominal logic, a first order theory of names and binding
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- Some lambda calculus and type theory formalized
- A very modal model of a modern, major, general type system
- Engineering formal metatheory
- Semantic types
- Barendregt’s Variable Convention in Rule Inductions
- A mechanical proof of the Church-Rosser theorem
- Residual theory in λ-calculus: a formal development
- Polymorphic regular tree types and patterns
- Theorem Proving in Higher Order Logics