Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 17:15 - 17:30 at CPP - Proof Tactics Chair(s): Jesper Cockx

Proof engineering efforts using interactive theorem proving have yielded several impressive projects in software systems and mathematics. A key obstacle to such efforts is the requirement that the domain expert is also an expert in the low-level details in constructing the proof in a theorem prover. In particular, the user needs to select a sequence of tactics that lead to a successful proof, a task that in general requires knowledge of the exact names of a large set of tactics.

We present Lassie, a tactic framework for the HOL4 theorem prover that allows individual users to define their own tactic language \emph{by example}, and for instance give frequently used tactics or tactic combinations easier-to-remember names. The core of Lassie is an extensible semantic parser, which allows the user to interactively extend the tactic language through a process of definitional generalization. Defining tactics in Lassie thus does not require any knowledge in tactic programming, while proofs written in Lassie retain the correctness guarantees provided by the HOL4 system. We show through case studies how Lassie can be used in small and larger proofs by novice and more experienced ITP users, and how we envision it to ease the learning curve in a HOL4 tutorial.

Presentation Slides (Lassie-CPP21.pdf)1.23MiB

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30: Proof TacticsCPP at CPP
Chair(s): Jesper CockxTU Delft

Streamed session: https://youtu.be/PAxUO84tUE8?t=3781

17:00 - 17:15
A Novice-Friendly Induction Tactic for Lean
Jannis LimpergVrije Universiteit Amsterdam
Pre-print Media Attached
17:15 - 17:30
Lassie: HOL4 Tactics by Example
Heiko BeckerMPI-SWS, Nathaniel BosMcGill University, Ivan GavranMPI-SWS, Eva DarulovaMPI-SWS, Rupak MajumdarMPI-SWS
Pre-print Media Attached File Attached