Harpoon: mechanizing metatheory interactively

DOI10.1007/978-3-030-79876-5_38OpenAlexW3181123080MaRDI QIDQ2055903

Brigitte Pientka, Jacob Errington, Junyoung Jang

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_38

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Harpoon ⋮ Harpoon: mechanizing metatheory interactively

Uses Software

• Coq
• Beluga
• Twelf
• Abella
• PoplMark
• Mtac

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Harpoon: mechanizing metatheory interactively
• Programming with binders and indexed data-types
• Programming Inductive Proofs
• Towards a mechanized metatheory of standard ML
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Inductive Beluga: Programming Proofs
• The Abella Interactive Theorem Prover (System Description)
• Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4
• A framework for defining logics
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• Mechanizing proofs with logical relations – Kripke-style
• An insider's look at LF type reconstruction: everything you (n)ever wanted to know
• POPLMark reloaded: Mechanizing proofs by logical relations
• Reconstructing proofs at the assertion level
• Contextual modal type theory
• Mtac: A monad for typed tactic programming in Coq

This page was built for publication: Harpoon: mechanizing metatheory interactively