Campus Event Calendar
Event Entry
What and Who
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.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 15 December 2008
14:00
60 Minutes
E1 5
019
Saarbrücken
Abstract
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.
Contact
Brigitta Hansen
0681 9325691
--email hidden
Video Broadcast
Yes
Kaiserslautern
49
204
passcode not visible
logged in users only
Brigitta Hansen, 11/28/2008 16:02
Brigitta Hansen, 11/27/2008 16:37 -- Created document.
Brigitta Hansen, 11/27/2008 16:37 -- Created document.