A solution to the PoplMark challenge based on de Bruijn indices

DOI10.1007/s10817-011-9230-5zbMath1260.68381OpenAlexW2006714020MaRDI QIDQ1945917

Jérôme Vouillon

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

zbMATH Keywords

theorem provingproof assistantsvariable bindingde Bruijn indicesmetatheory\texttt{Coq}

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Uses Software

• Coq
• PoplMark
• Nominal Isabelle

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