Liberating Semi-Automated PL Proofs from Binder Bookkeeping
Post date: Feb 8, 2009 6:19:39 PM
The advantages of machine-checked proofs about programming languages have been clear for decades now, and the POPLmark Challenge has helped get more PL researchers started building such formal proofs. Unfortunately, almost everyone not doing research in proof assistants finds the state-of-the-art extremely cumbersome. The most popular encoding schemes for general-purpose proof assistants like Coq and Isabelle/HOL involve so much bookkeeping about variables that such "obvious" theorems usually make up a majority of a formal development. Systems like Twelf enable the use of higher-order abstract syntax, but they require that every step of every proof be written out manually in complete detail, and they are intrinsically less well-suited to verification of functional programs and to theorem-proving about domains beyond syntactic metatheory.
In this talk, I will present a way of getting (most of) the best of both worlds, via parametric higher-order abstract syntax. This technique makes it possible to define syntax tree datatypes so that every well-typed AST is well-formed, by construction, in contrast to the more standard Coq and Isabelle methodologies. Moreover, it is easy to write functions, like compiler transformations, whose types guarantee that they manipulate syntax correctly. We can build mostly-automated correctness proofs of such transformations without ever once mentioning syntactic substitution, the subject of the bulk of proof effort
with previous techniques.
Date: Feb 11, 2009
Speaker: Adam Chlipala, Harvard University