Campus Event Calendar
Event Entry
What and Who
Interactive Typed Tactic Programming in Coq
Beta Ziliani
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 26 November 2013
16:00
60 Minutes
E1 5
029
Saarbrücken
Abstract
Effective support for custom proof automation is essential for large-scale
interactive proof development. However, existing languages for automation
via tactics either (a) provide no way to specify the behavior of tactics
within the base logic of the accompanying theorem prover, or (b) rely on
advanced type-theoretic machinery that is not easily integrated into
established theorem provers.
My thesis is that typechecked tactic programming in Coq is possible in two
different programming styles: (1) logic programming (by exploiting Coq’s
existing overloading mechanism) and (2) functional programming (by a new
monadic language, Mtac). The combination of both styles leads to a novel
way of creating extensible tactics.
interactive proof development. However, existing languages for automation
via tactics either (a) provide no way to specify the behavior of tactics
within the base logic of the accompanying theorem prover, or (b) rely on
advanced type-theoretic machinery that is not easily integrated into
established theorem provers.
My thesis is that typechecked tactic programming in Coq is possible in two
different programming styles: (1) logic programming (by exploiting Coq’s
existing overloading mechanism) and (2) functional programming (by a new
monadic language, Mtac). The combination of both styles leads to a novel
way of creating extensible tactics.
Contact
--email hidden
passcode not visible
logged in users only
Brigitta Hansen, 11/29/2013 15:26
Maria-Louise Albrecht, 11/26/2013 10:21 -- Created document.
Maria-Louise Albrecht, 11/26/2013 10:21 -- Created document.