Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Interactive Typed Tactic Programming in the Coq Proof Assistant
Speaker:Luis Francisco Ziliani
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Defense
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Tuesday, 24 March 2015
Duration:60 Minutes
Building: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.
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:112
Tags, Category, Keywords and additional notes
Attachments, File(s):
Created by:Maria-Louise Albrecht/MPI-KLSB, 03/23/2015 09:30 AMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:14 PM
  • Maria-Louise Albrecht, 03/23/2015 09:46 AM
  • Maria-Louise Albrecht, 03/23/2015 09:44 AM -- Created document.