There is a signup schedule for this event.

Spea

ker Name/Affiliation: Robert Harper/Carnegie Mellon University

Talk
Title: Mechanizing the Meta-theory of Programming Languages

Date/T

ime: February 10 2005 at 11:00 a.m.

Coffee: 10:45 a.m.

Loca

tion: ACES 2.302

Host: William Cook

Talk Abstract:
What

does it mean for a programming language to exist?
Usually languages ar

e defined by an informal description
augmented by a reference compiler

whose behavior is regarded
as normative. This approach works well so l

ong as the one
true implementation suffices but as soon as we wish to

have multiple compilers for the same language we must agree
on wha

t the language is independently of its implementations.
Most often thi

s is accomplished through social processes
such as standardization comm

ittees for building consensus.

These processes have served us well

and will continue to
be important for language design. But they are no

t sufficient
to support the level of rigor required to prove theorems <

br>about languages and programs written in them. For that
we need a se

mantics which provides an objective foundation
for such analyses typi

cally in the form of a type system
and an operational semantics. But me

rely having such a rigorous
definition for a language is not enough ---
it must be validated
by a body of meta-theory that establishes its coh

erence
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. Th

e 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 t

o express and enforce crucial invariants in
our programs. I will descr

ibe our use of the Twelf implementation
of the LF logical framework an

d discuss our successes and
difficulties in using it as a tool for mech

anizing the meta-theory
of programming languages.

Speaker Bio:Robert Harper is a professor in the Computer Science Department
at Ca

ng languages and the application of type theory
to the description and
analysis of hybrid systems.