Putting Curry-Howard to Work

Putting Curry-Howard to Work by Tim Sheard.

This paper describes some type system feature suggested by the Curry-Howard isomorphism (which states that types are propositions and that programs are their proofs). The language Ωmega is a descendant of Haskell in which the author has implemented all of the features described in the paper.

I still haven't finished reading it, but it's at the top of my pile.

DOI | Del.icio.us | CiteULike | LtU