An open challenge problem repository for systems supporting binders

DOI10.4204/EPTCS.185.2MaRDI QIDQ6940457zbMATH OpenFDO

Authors Amy P. Felty, Alberto Momigliano, Brigitte Pientka

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.185.2

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Digital mathematics libraries and repositories (68V35)

Cites work

• A two-level logic approach to reasoning about computations
• An overview of the K semantic framework
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• One logic to use them all
• Ott: Effective tool support for the working semanticist
• Programming with binders and indexed data-types
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• SATLIB: An online resource for research on SAT
• Semantics engineering with PLT Redex
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• The Abella Interactive Theorem Prover (System Description)
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The Twelf Proof Assistant
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Theorem Proving in Higher Order Logics
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• Types and programing languages

This page was built for publication: An open challenge problem repository for systems supporting binders

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