Campus Event Calendar

Event Entry

What and Who

Interactive Typed Tactic Programming in the Coq Proof Assistant

Luis Francisco Ziliani
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
Public Audience

Date, Time and Location

Tuesday, 24 March 2015
60 Minutes
E1 5


Proof assistants like Coq are now eminently effective for formalizing
"research-grade" mathematics, verifying serious software systems, and,
more broadly, enabling researchers to mechanize and breed confidence
in their results. Nevertheless, the mechanization of substantial
proofs typically requires a significant amount of manual effort. To
alleviate this burden, proof assistants typically provide an
additional language for tactic programming. Tactics support
general-purpose scripting of automation routines, as well as fine
control over the state of an interactive proof. However, for most
existing tactic languages (e.g., ML, Ltac), the price to pay for this
freedom is that the behavior of a tactic lacks any static
specification within the base logic of the theorem prover (such as, in
Coq, a type). As a result of being untyped, tactics are known to be
difficult to compose, debug, and maintain.

In my thesis I present two different approaches to typed tactic
programming in the context of Coq: Lemma Overloading and Mtac. Both
approaches rely heavily on the unification algorithm of Coq, which is
a complex mixture of different heuristics and has not been formally
specified. Therefore, I also build and describe a new unification
algorithm better suited for tactic programming in Coq. In the talk I
will describe the high level achievements of my work and introduce in
depth Mtac, a new programming language for tactic programming.


--email hidden

Video Broadcast

passcode not visible
logged in users only

Maria-Louise Albrecht, 03/23/2015 09:46
Maria-Louise Albrecht, 03/23/2015 09:44 -- Created document.