Formalizing adequacy: a case study for higher-order abstract syntax
From MaRDI portal
Publication:2392483
DOI10.1007/S10817-011-9221-6zbMATH Open1269.68042OpenAlexW2099835716MaRDI QIDQ2392483FDOQ2392483
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
Recommendations
Cites Work
- Nominal techniques in Isabelle/HOL
- Logical frameworks
- Alpha-structural recursion and induction
- A framework for defining logics
- Title not available (Why is that?)
- A new approach to abstract syntax with variable binding
- Types for Proofs and Programs
- Proof Pearl: De Bruijn Terms Really Do Work
- Mechanizing metatheory in a logical framework
- Uniform proofs as a foundation for logic programming
- The representational adequacy of <scp>Hybrid</scp>
- Title not available (Why is that?)
- Equivalences between logics and their representing type theories
- Barendregt’s Variable Convention in Rule Inductions
- Mechanizing the metatheory of LF
- A third-order representation of the \(\lambda\mu\)-calculus
- Formalising in nominal Isabelle Crary's completeness proof for equivalence checking
- Nominal system T
Cited In (2)
Uses Software
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)
