The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey

DOI10.1007/S10817-015-9327-3zbMath1357.68198OpenAlexW1551936078MaRDI QIDQ287277

Alberto Momigliano, Brigitte Pientka, Amy P. Felty

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9327-3

zbMATH Keywords

benchmarkshigher-order abstract syntaxproof assistantscontext reasoninglogical frameworks

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (14)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Inductive Beluga: Programming Proofs ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Canonical HybridLF: extending Hybrid with dependent types ⋮ Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ Unnamed Item ⋮ Harpoon: mechanizing metatheory interactively ⋮ Mechanized metatheory revisited ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ Formal meta-level analysis framework for quantum programming languages ⋮ Mechanizing focused linear logic in Coq ⋮ Rensets and renaming-based recursion for syntax with bindings

Uses Software

• Coq
• HYBRID
• Beluga
• Twelf
• Abella
• Toolchain
• Vellvm

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• Nominal abstraction
• Verifying termination and reduction properties about higher-order logic programs
• Cut elimination for a logic with induction and co-induction
• A two-level logic approach to reasoning about computations
• On the Expressivity of Minimal Generic Quantification
• Explicit Contexts in LF (Extended Abstract)
• Case Analysis of Higher-Order Data
• Programming with Higher-Order Logic
• Programming with binders and indexed data-types
• Formalizing the LLVM intermediate representation for verified program transformations
• Verified Software Toolchain
• Programming Inductive Proofs
• The Twelf Proof Assistant
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• The Abella Interactive Theorem Prover (System Description)
• A Coverage Checking Algorithm for LF
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
• A framework for defining logics
• Proof Pearl: Abella Formalization of λ-Calculus Cube Property
• Contextual modal type theory
• Mechanizing metatheory in a logical framework
• Reasoning with higher-order abstract syntax in a logical framework
• Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

This page was built for publication: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey