Colloquia: Robert Harper/Carnegie Mellon University Mechanizing the Meta-theory of Programming Languages in ACES 2.302
There is a signup schedule for this event.
ker Name/Affiliation: Robert Harper/Carnegie Mellon University
Title: Mechanizing the Meta-theory of Programming Languages
ime: February 10 2005 at 11:00 a.m.
Coffee: 10:45 a.m.
tion: ACES 2.302
Host: William Cook
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
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
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
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
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
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
of Standard ML; the design and application of the LF logical
framework; the type-theoretic foundations of modularity
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
His current interests include the development of a trust-free
framework for grid computing enriching the type structure
ng languages and the application of type theory
to the description and
analysis of hybrid systems.
- Awards & Honors
- About Us
- Student Engagement and Support
- Masters Program
- Ph.D. Program
- Financial Information
- Prospective Students
- Incoming Students
- Current Students
- Curricular Practical Training
- Grad Student Talks
- UTCS Direct