Colloquia: Robert Harper/Carnegie Mellon University Mechanizing the Meta-theory of Programming Languages in ACES 2.302

Contact Name: 
Jenna Whitney
Date: 
Feb 10, 2006 11:00am - 12:00pm


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

rnegie 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 Fo

undations of Computer
Science at Edinburgh University from 1985-1988.

He is best
known for his work on the design definition and implementa

tion
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 comp

ilation; the co-invention of
self-adjusting computation for dynamic al

gorithms; and the
application of fundamental theory to practical syste

ms.
His current interests include the development of a trust-free

framework for grid computing enriching the type structure
of programmi

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