The Curry-Howard correspondence is a mapping between logic and type systems. On the one hand you have logic systems with propositions and proofs. On the other hand you have type systems with types and programs (or functions). As it turns out these two very different things have very similar rules. This article will explore the Curry-Howard correspondence by constructing a proof system using the Haskell type system (how appropriate since Haskell is named after Haskell Curry, the "Curry" in "Curry-Howard"). We'll set up the rules of logic using Haskell types and programs. Then we'll use these rules as an abstract interface to perform some logic profs.
Epigram is a dependently typed programming language and an interactive programming environment. Epigram has got a type system which is strong enough to express the behaviour of programs, the type checker then guarantees that the program is well behaved. However, you don't have to go as far, you can write ordinary programs and refactor them into more trustworthy, formally checked deliverables -- Epigram supports a pay as you go approach to formal methods. Epigram is freely available this page provides access to downloads of version 1 as source or binaries for the major platforms along with relevant documentation. Development on version 2 is under way we hope this will considerably improve on the first, and details of its current state are available, in the form of a developers' 'blog.
Interpreting types as abstract values [The Abstract of the lecture notes] We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type checking, deals with approximations like int. A type system is sound if it correctly approximates the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has the type int, the dynamic evaluation of the term, if it terminates, will yield an integer. As object language, we use simply-typed and let-polymorphic lambda calculi with integers and integer operations as constants. We use Haskell as a metalanguage in which to write evaluators, type checkers, type reconstructors and inferencers for the object language.