Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions

DOI10.1017/S0960129517000093zbMath1400.68194MaRDI QIDQ4691183

Alberto Momigliano, Brigitte Pientka, Amy P. Felty

Publication date: 19 October 2018

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Related Items (4)

POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Harpoon: mechanizing metatheory interactively ⋮ Mechanized metatheory revisited ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic

Uses Software

• HYBRID
• SATLIB
• TPTP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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 two-level logic approach to reasoning about computations
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• Mechanizing metatheory in a logical framework

This page was built for publication: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions