[PRL] [Fwd: Harper at MIT Oct 2 4pm]

[Dave Herman]

FYI-- tomorrow afternoon at MIT.

Dave

-------- Original Message --------
Subject: Harper at MIT Oct 2 4pm
Date: Wed, 01 Oct 2008 20:29:30 -0400
From: David Van Horn <dvanhorn at ccs.neu.edu>
To: Dave Herman <dherman at ccs.neu.edu>

[ Dave, would you fwd this to PRL? ]

Mechanizing the Metatheory of Programming Languages
Speaker: Robert Harper, Carnegie Mellon University
Date: Thursday, October 2 2008
Time: 4:00PM to 5:30PM
Refreshments: 3:45PM
Location: 32-G449(Patil)
Host: Martin Rinard, CSAIL
Contact: Colleen Russell, 3-0145, crussell at csail.mit.edu
Relevant URL:
http://www.csail.mit.edu/events/eventcalendar/calendar.php?show=event&id=1786


Abstract:
What does it mean for a programming language to exist? Languages are
usually defined by an informal description augmented by a reference
compiler whose behavior is regarded as normative. This approach works
well so long as a single reference compiler suffices, but as soon as
there are multiple implementations, it is necessary agree on what
language they implement. This is typically achieved through social
processes such as standardization committees that build consensus and
impose norms.

These processes have served us well, and will continue to be important
for language design. But they are not sufficient to support the level of
rigor required to prove theorems about languages and programs written in
them. For that we need a semantics, which provides an objective
foundation for such analysis. But merely having such a rigorous
definition for a language is not enough --- it must be validated by a
body of meta-theory that establishes its coherence and its consistency
with expectations.

But how are we to develop and maintain this body of theory? For
full-scale languages the task is so onerous as to inhibit innovation and
foster stagnation. The way forward is to take advantage of the recent
advances in mechanized reasoning. By representing a language definition
within a logical framework we may subject it to formal analysis, much as
we use types to express and enforce crucial invariants in our programs.
I will describe the use of the Twelf implementation of the LF logical
framework, and discuss the successes and difficulties in using it as a
tool for mechanizing the meta-theory of programming languages.