Formalizing adequacy: a case study for higher-order abstract syntax

DOI10.1007/s10817-011-9221-6zbMath1269.68042OpenAlexW2099835716MaRDI QIDQ2392483

James Cheney, Michael Norrish, René Vestergaard

Publication date: 1 August 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-011-9221-6

zbMATH Keywords

isomorphismhigher-order abstract syntaxinterpretationadequacynominal abstract syntax

Mathematics Subject Classification ID

Uses Software

• Isabelle/HOL
• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Nominal techniques in Isabelle/HOL
• Uniform proofs as a foundation for logic programming
• A Third-Order Representation of the λμ-Calculus
• Mechanizing the metatheory of LF
• The representational adequacy of <scp>Hybrid</scp>
• Proof Pearl: De Bruijn Terms Really Do Work
• Alpha-structural recursion and induction
• Barendregt’s Variable Convention in Rule Inductions
• A framework for defining logics
• Equivalences between logics and their representing type theories
• Nominal system T
• Mechanizing metatheory in a logical framework
• Types for Proofs and Programs

This page was built for publication: Formalizing adequacy: a case study for higher-order abstract syntax