[Colloquium] Talk by Robert Harper, Carnegie Mellon University, 6/27/05

[Margery Ishmael]

DEPARTMENT OF COMPUTER SCIENCE

Date: Monday, June 27, 2005

Time: 2:00 p.m.
Place: Ryerson 251

-------------------------------------------

Speaker:  ROBERT HARPER, Carnegie Mellon University

Url:  http://www-2.cs.cmu.edu/~rwh/

Title:  Mechanizing Metatheory Using Twelf

Abstract:

What does it mean for a programming language to exist?  The usual
approach is to define a language by a "reasonably precise" description
a la K&R, together with a "reference compiler" that implements it (and
serves as the final arbiter of ambiguities).  This relies heavily on
social constructs such as standardization committees, or on the
marketing clout of a large corporation, and is not suitable as a basis
for a rigorous analysis of the safety or security properties of the
language.

Another approach is to define a language by a rigorous semantics that
is amenable to mathematical analysis.  The most successful method of
semantic definition is to give a static semantics in the form of a
type system and a dynamic semantics in the form of execution rules for
a program.  This gives the definition an objective character that is
amenable to analysis, and helps to ensure the compatibility of
compilers for it.  But having a rigorous definition is not enough; at
a minimum one must prove that it is internally coherent according to
various criteria.  This re-introduces some of the difficulties of the
traditional methods, because someone has to do the proofs and someone
has to read them to ensure they are right.  The burdens of doing "at
scale" are so severe that the semantics becomes an inhibitor, rather
than an enabler, of innovation.

One way forward is to formalize the definition within a logical
framework and to use verification tools to check crucial properties,
much as we use type systems to ensure sensibility of our programs.  I
will describe the work we have been doing on mechanizing formal
language definitions, and describe some of the successes, and
difficulties, of using the Twelf system to verify their metatheory.

Joint work with Karl Crary and Michael Ashley-Rolman.

-------------------------------------------------------

Host: David B. MacQueen

*Refreshments will be served after the talk in Ryerson 255*

People in need of assistance should call 773-834-8977 in advance.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/enriched
Size: 2386 bytes
Desc: not available
Url : http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20050623/ba4ca50d/attachment.bin