[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, February 18, 2009
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Adam Chlipala
Harvard University

Liberating Semi-Automated PL Proofs from Binder Bookkeeping

Abstract:

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.

================================================================

Upcoming Events:

# Nothing scheduled :-(  Wouldn't you like to give a talk?

--Mitch