2007/11-19
From SIPB Cluedumps
(update with Jesse's new version) |
(better context) |
||
| Line 3: | Line 3: | ||
|date=2007-11-19 20:30 | |date=2007-11-19 20:30 | ||
|location=56-114 | |location=56-114 | ||
| - | |notes= '''UPDATE''' May 2008: Jesse has [http://www.ccs.neu.edu/home/tov/session-types/ a new implementation] complete with a paper explaining it | + | |notes= '''UPDATE''' May 2008: Jesse has [http://www.ccs.neu.edu/home/tov/session-types/ a new implementation] of session types, complete with a paper explaining it and prototype implementations in five other languages. |
See [http://web.mit.edu/price/a/2007/haskell/slides.pdf slides], and (tarball) [http://web.mit.edu/price/a/2007/haskell/examples.tar.gz code examples]. | See [http://web.mit.edu/price/a/2007/haskell/slides.pdf slides], and (tarball) [http://web.mit.edu/price/a/2007/haskell/examples.tar.gz code examples]. | ||
Latest revision as of 07:48, 24 May 2008
[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. |
