Events

22 October 2008

Wednesday 22 October 2008, 11h, batiment I, 1er étage

Mechanizing the Metatheory of Programming Languages
Bob Harper
Carnegie-Mellon University

Program verification is difficult, and remains a task for specialists. One way to bring verification into wider use is through the design of rich type systems that guarantee useful safety properties of all programs written in that language. This shifts the burden of verification of these properties from the programmer to the language designer: one theorem about a language induces an instance of that theorem for every program written in that language.

Over the last few decades very effective methods have been developed for precisely defining programming languages, the most widely used being type systems and operational semantics. Many advances have been made in language design, and many methods have been developed for proving properties of them. But even small prototype languages are rather unwieldy objects of study, involving many cases and detailed arguments that are difficult to check thoroughly by hand.

Consequently, much effort is being concentrated mechanizing the metatheory of programming languages, using a variety of approaches. At Carnegie Mellon we make daily use of the Twelf implementation of the LF logical framework as an essential tool for language design. It has been applied to dozens of small examples, and, recently, to a full-scale language, Standard ML. In this talk I will describe our use of Twelf for mechanizing metatheory, and our ongoing effort to produce a fully machine-checked proof of type safety for Standard ML.

Bob Harper will be visiting from 20 October to 24 October.