BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:How to Make Ad Hoc Proof Automation Less Ad Hoc - Derek Dreyer
DTSTART:20110517T090000Z
DTEND:20110517T100000Z
UID:TALK31389@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Most interactive theorem provers provide support for some form
  of user-customizable proof automation.  In a number of popular systems\, 
 such as Coq and Isabelle\, this automation is achieved primarily through *
 tactics*\, which are programmed in a separate language from that of the pr
 over's base logic.  While tactics are clearly useful in practice\, they ca
 n be difficult to maintain and compose because\, unlike lemmas\, their beh
 avior cannot be specified within the expressive type system of the prover 
 itself.\n\nWe propose a novel approach to proof automation in Coq that all
 ows the user to specify the behavior of custom automated routines in terms
  of Coq's own type system.  Our approach involves a sophisticated applicat
 ion of Coq's *canonical structures*\, which generalize Haskell type classe
 s and facilitate a flexible style of dependently-typed logic programming. 
  Specifically\, just as Haskell type classes are used to infer the canonic
 al implementation of an overloaded term at a given type\, canonical struct
 ures can be used to infer the canonical *proof* of an overloaded *lemma* f
 or a given instantiation of its parameters.  We present a series of design
  patterns for canonical structure programming that enable one to carefully
  and predictably coax Coq's type inference engine into triggering the exec
 ution of user-supplied algorithms during unification\, and we illustrate t
 hese patterns through several realistic examples drawn from Hoare Type The
 ory.  We assume no prior knowledge of Coq and describe the relevant aspect
 s of Coq type inference from first principles.\n\nThis is joint work with 
 Georges Gonthier\, Aleks Nanevski\, and Beta Ziliani.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR