Interactive Typed Tactic Programming
in the Coq Proof Assistant
Author: Beta Ziliani
Supervisor: Derek Dreyer
I motivate the different characteristics of Lemma Overloading and Mtac through a wide range of examples, mainly coming from program verification. I also show how to combine these approaches in order to obtain the best of both worlds, resulting in extensible, typed tactics that can be programmed interactively.
Both approaches rely heavily on the unification algorithm of Coq, which currently suffers from two main drawbacks: it incorporates heuristics not appropriate for tactic programming, and it is undocumented. In this dissertation, in addition to the aforementioned approaches to tactic programming, I build and describe a new unification algorithm better suited for tactic programming in Coq.
- Manuscript [pdf]
- Code [zip] (See INSTALL file from the distribution.)
- Video: Click to show/hide.