Harpoon: Mechanizing Metatheory Interactively
Jacob Errington, Junyoung Jang, Brigitte Pientka · Lecture notes in computer science · 2021
Abstract Belugais a proof checker that provides sophisticated infrastructure for implementing formal systems with the logical framework LF and proving metatheoretic properties as total, recursive functions transforming LF derivations. In this paper, we describeHarpoon, an interactive proof engine built on top ofBeluga. It allows users to develop proofs interactively using a small, fixed set of high-levelactionsthat safely transform a subgoal. A sequence of actions elaborates into a (partial)proof scriptthat serves as an intermediate representation describing an assertion-level proof. Last, a proof script translates into aBelugaprogram which can be type-checked independently.Harpoonis available on GitHub. We have usedHarpoonto replay a wide array of examples covering all features supported byBeluga. In particular, we have used it for normalization proofs, including the recently proposed POPLMark reloaded challenge.