Mechanizing the Metatheory of Programming Languages
Robert Harper
Carnegie Mellon University
SWS Distinguished Lecture Series - Winter
Robert Harper is a professor in the Computer Science Department at Carnegie Mellon University, where he has been a faculty member since 1988. He received his Ph.D. in Computer Science from Cornell University in 1985, and was a post-doctoral research fellow at the Laboratory for Foundations of Computer Science at Edinburgh University from 1985-1988. He is best known for his work on the design, definition, and implementation of Standard ML; the design and application of the LF logical framework; the type-theoretic foundations of modularity in programming languages; the use of typed intermediate languages for certified compilation; the co-invention of self-adjusting computation for dynamic algorithms; and the application of fundamental theory to practical software systems. His current interests include mechanization of the metatheory of programming languages, the integration of types and verification, and the application of programming language theory to computer security.
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.