Harpoon: Mechanizing Metatheory Interactively

Beluga is 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 describe Harpoon, an interactive proof engine built on top of Beluga. It allows users to develop proofs interactively using a small, fixed set of high-level actions that safely transform a subgoal. A sequence of actions elaborates into a (partial) proof script that serves as an intermediate representation describing an assertion-level proof. Last, a proof script translates into a Beluga program which can be type-checked independently. Harpoon is available on GitHub. We have used Harpoon to replay a wide array of examples covering all features supported by Beluga. In particular, we have used it for normalization proofs, including the recently proposed POPLMark reloaded challenge.

A Unified View of Induction Reasoning for First-Order Logic

Induction is a powerful proof technique adapted to reason on setswith an unbounded number of elements. In a first-order setting, twodifferent methods are distinguished: the conventional induction,based on explicit induction schemas, and the implicit induction,based on reductive procedures. We propose a new cycle-basedinduction method that keeps their best features, i.e. i) performslazy induction, ii) naturally fits for mutual induction, and iii) isfree of reductive constraints. The heart of the method is a proofstrategy that identifies in the proof script the subset of formulascontributing to validate the application of induction hypotheses.The conventional and implicit induction are particular cases of ourmethod.

A pluralist approach to the formalisation of mathematics

We present a programme of research for pluralist formalisations, that is, formalisations that involve proving results in more than one foundation.A foundation consists of two parts: a logical part, which provides a notion of inference, and a non-logical part, which provides the entities to be reasoned about. An LTT is a formal system composed of two such separate parts. We show how LTTs may be used as the basis for a pluralist formalisation.We show how different foundations may be formalised as LTTs, and also describe a new method for proof reuse. If we know that a translation Φ exists between two logic-enriched type theories (LTTs) S and T, and we have formalised a proof of a theorem α in S, we may wish to make use of the fact that Φ(α) is a theorem of T. We show how this is sometimes possible by writing a proof script MΦ. For any proof script Mα that proves a theorem α in S, if we change Mα so it first imports MΦ, the resulting proof script will still parse, and will be a proof of Φ(α) in T.In this paper, we focus on the logical part of an LTT-framework and show how the above method of proof reuse is done for four cases of Φ: inclusion, the double negation translation, the A-translation and the Russell–Prawitz modality. This work has been carried out using the proof assistant Plastic.