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

DOI10.1007/S10817-011-9221-6MaRDI QIDQ2392483zbMATH OpenOpenAlexFDO

Authors 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

interpretationadequacyisomorphismhigher-order abstract syntaxnominal abstract syntax

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1701361
• Nominal techniques in Isabelle/HOL
• Higher-order abstract syntax in Isabelle/HOL
• The representational adequacy of Hybrid
• The theory of contexts for first order and higher order abstract syntax

Cites work

• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 1007358 (Why is no real title available?)
• A framework for defining logics
• A new approach to abstract syntax with variable binding
• A third-order representation of the \(\lambda\mu\)-calculus
• Alpha-structural recursion and induction
• Barendregt’s Variable Convention in Rule Inductions
• Equivalences between logics and their representing type theories
• Formalising in nominal Isabelle Crary's completeness proof for equivalence checking
• Logical frameworks
• Mechanizing metatheory in a logical framework
• Mechanizing the metatheory of LF
• Nominal system T
• Nominal techniques in Isabelle/HOL
• Proof Pearl: De Bruijn Terms Really Do Work
• The representational adequacy of Hybrid
• Types for Proofs and Programs
• Uniform proofs as a foundation for logic programming

Cited in

(2)

• Assessing the Expressivity of Formal Specification Languages
• A syntactic view of computational adequacy

Describes a project that uses

Uses Software

• Nominal Isabelle
• Isabelle/HOL

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2392483)