Abstract
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: http://www.mpi-sws.org/~beta/lessadhoc/
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.
Resources
This will be shown to users with no Flash or Javascript.
|
