ROSAEC center Seoul National University

Seminars & Workshops

Speaker:Derek Dreyer , Max Planck Institute for Software Systems
When:2011-09-15 14:00
Place:Room 309, Bldg 302, SNU


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 prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself. We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's *canonical structures*, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical *proof* of an overloaded *lemma* for 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 execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles. This is joint work with Georges Gonthier, Aleks Nanevski, and Beta Ziliani. Our accompanying ICFP'11 paper and Coq source is available at the following URL:

Short bio

Derek Dreyer obtained his PhD in Computer Science from Carnegie Mellon University in 2005 under the supervision of Bob Harper and Karl Crary. He was a research assistant professor at the Toyota Technological Institute at Chicago from 2005 to 2007. Since 2008, he has held the position of independent researcher (tenure-track faculty) at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany, where he leads the Type Systems and Functional Programming group. Derek's research focuses on the design, semantics, and verification of modern programming languages, with an emphasis on module systems and compositional reasoning.


© Copyright 2008-2010 ROSAEC Center, Seoul National University