[Pl-seminar] Talk at Harvard, Thursday, Oct. 6: Tim Sheard

[Norman Ramsey]

pl-seminar folks might be interested in the following talk.


Norman



Harvard University
Computer Science Colloquium Series
33 Oxford St.
 Cambridge, MA 02138

Colloquium

Putting the Curry-Howard Isomorphism to work

Tim Sheard
Professor of Computer Science
Portland State University
        
Thursday, October 6, 2005
4:00PM
Maxwell Dworkin G125
(Ice Cream at 3:30PM - Maxwell Dworkin 2nd Floor Lounge Area)
    
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.

Web-location: http://www.cs.pdx.edu/~sheard/

Host:    Professor Norman Ramsey