Colloquium Details
Putting the Curry-Howard Isomorphism to Work
| Author: | Tim Sheard Portland State University |
|---|---|
| Date: | November 30, 2006 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
| Host: | Yannis Smaragdakis |
Abstract
There has been a lot of recent interest in exploiting the Curry-Howard isomorphism in type systems for more or less traditional programming languages. Types based upon the Curry-Howard isomorphism can express precise properties of programs. Such properties can be either functional or non-functional properties. I.e. they can constrain either the output of the program, or the resources needed to produce the output, or both. In the talk I will introduce the basic ideas from scratch, and give many, many examples that illustrate its use. The talk is not addressed at experts in type systems, but to general computer scientists who are interested in describing properties of their progams precisely.
Our goal is to build a system in which the specification of designs, the definition of properties, the implementation of programs, and the checking that programs adhere to their properties, are all bundled in a coherent manner into a single unified system that appears to the user to be a programming language. We hope to use our system as a broad spectrum language, capable of handling abstract properties as well as implementation minutiae, where the connection between properties and programs is formal and precise.
Biography
Tim Sheard obtained his 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) with broad influence on the programming language community.