A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL

DOI10.1007/s10817-011-9231-4zbMath1260.68366OpenAlexW2077540255MaRDI QIDQ1945915

Stefan Berghofer

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

zbMATH Keywords

lambda calculustype systemsformalized metatheory

Mathematics Subject Classification ID

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

Related Items

A solution to the PoplMark challenge based on de Bruijn indices

Uses Software

• Coq
• ML
• Isabelle/HOL
• Twelf
• PoplMark
• Nominal Isabelle

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