Putting the Curry-Howard Isomorphism to Work

Tim Sheard

Portland State University

FAB 310
Oct 31st, 2005
12-1pm

ABSTRACT
The Curry-Howard isomorphism states that types are propositions and that

programs are proofs. This allows programmers to state and enforce invariants

of programs by using types. Unfortunately, the type systems of today's functional

languages cannot directly express interesting properties of programs. To
alleviate this problem, we propose the addition of three new features
to functional programming languages such as Haskell: Generalized
Algebraic Datatypes, Extensible Kind Systems, and the generation,
propagation, and discharging of Static Propositions.  These three new
features are backward compatible with existing features, and combine
to enable a new programming paradigm for functional programmers. This
paradigm makes it possible to state and enforce interesting
properties of programs using the type system, and it does this in a
manner that leaves intact the functional programming style, known and
loved by functional programmers everywhere.


BIOGRAPHY
Tim Sheard obtained is Ph.D. Computer and Information Science, at the
University of Massachusetts, Amherst in 1985, and is currently
Professor of Computer Science at Portland State University. His
research interests include: Program Generation, Meta-Programming
Systems, Theorem Proving, Logical Frameworks, Type Systems, Domain
Specific Languages, and Patterns for Functional Programming. He was
the General Chair of Generative Programming and Component Engineering
(GPCE'04), and was organizer of the 2001 ICFP Programming Contest which
attracted over 250 entries from around the world. He is a pioneer in the
area of meta-programming and is the creator of three research artifacts
(MetaML, Template Haskell, and the Omega Programming Language) that
have had a broad influence on the programming language community.

HOST

Nirupama Bulusu