Harpoon: mechanizing metatheory interactively
From MaRDI portal
Publication:2055903
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
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
Uses Software
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