Reasoning with higher-order abstract syntax and contexts: a comparison

DOI10.1007/978-3-642-14052-5_17zbMATH Open1291.68340OpenAlexW2139128755MaRDI QIDQ5747652FDOQ5747652

Authors 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

Recommendations

• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Reasoning with higher-order abstract syntax in a logical framework
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax

Cited in

(11)

• Scalable algorithms for abduction via enumerative syntax-guided synthesis
• Programming inductive proofs. A new approach based on contextual types
• A formalized general theory of syntax with bindings: extended version
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• scientific article; zbMATH DE number 7204440 (Why is no real title available?)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• Mechanizing proofs with logical relations -- Kripke-style
• Reasoning with higher-order abstract syntax in a logical framework
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• Case analysis of higher-order data

Describes a project that uses

Uses Software

• Beluga
• Tac
• Abella
• PoplMark

This page was built for publication: Reasoning with higher-order abstract syntax and contexts: a comparison

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