Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison

DOI10.1007/978-3-642-14052-5_17zbMath1291.68340OpenAlexW2139128755MaRDI QIDQ5747652

Brigitte Pientka, Amy P. Felty

Publication date: 14 September 2010

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_17

Mathematics Subject Classification ID

Related Items

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, A formalized general theory of syntax with bindings: extended version, Programming Inductive Proofs, Mechanizing proofs with logical relations – Kripke-style, Unnamed Item

Uses Software

• Beluga
• Tac
• Abella
• PoplMark