From SIPB Cluedumps

Jump to: navigation, search

[edit] Haskell: Compiler as Theorem-Prover

Date: November 19, 2007, at 3:30 PM
Presenters: Greg Price (price)
Location: 56-114
Notes: UPDATE May 2008: Jesse has a new implementation of session types, complete with a paper explaining it and prototype implementations in five other languages.

See slides, and (tarball) code examples.

For STM, see Simon Peyton Jones' gentle introduction, or a paper applying STM to lock-free data structures.

For protocol/session types, see the literature, or check out Oleg Kiselyov's work, particularly "HList", for some of the tools that make Jesse Tov's Haskell implementation, which I presented, possible. Or look at Jesse's web page to see if he's put up a paper or a new version. UPDATE: he has, see above.

For "theorems for free", see Phil Wadler's 1989 and later writeups.

For a broad overview of the Curry-Howard correspondence ("proofs are programs, programs proofs"), see more Phil Wadler, particularly his 2000 writeup.

Abstract: Haskell is the world's most *reasonable* programming language. Every language's optimizing compilers reason about programs, and every programmer reasons about the code they write ("this loop never indexes this array out of bounds"; "this resource is never accessed without holding the lock") -- but in no more mainstream language do the compiler and the programmer have an adequate medium in which to communicate about their reasoning: a rich static type system. In Haskell the programmer has in the type system a powerful theorem-prover ready at hand, and if the programmer's theorem is of the form "task X can be done", the compiler's proof can be the very code that carries out task X.

This cluedump will briefly introduce Haskell and its type system, describe the Curry-Howard isomorphism between code with types and propositions with proofs, and show you how you can make a Haskell implementation verify the units you attach to physical quantities; guarantee code to be free of side effects; write code for you to traverse a complicated data structure; and guarantee your lock-free code threadsafe with software transactional memory.

Personal tools