Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
From MaRDI portal
Publication:4691183
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)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
