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

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

Mathematics Subject Classification ID

Cited In (8)

• 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
• Reasoning with higher-order abstract syntax in a logical framework
• Mechanizing proofs with logical relations – Kripke-style
• Title not available (Why is that?)
• Programming inductive proofs. A new approach based on contextual types
• Scalable algorithms for abduction via enumerative syntax-guided synthesis

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)