2007/11-19

From SIPB Cluedumps

(Difference between revisions)
Jump to: navigation, search
(clarify Jesse's relationship to the session-types work, per his own scruples; also link Oleg's work)
(update with Jesse's new version)
Line 3: Line 3:
|date=2007-11-19 20:30
|date=2007-11-19 20:30
|location=56-114
|location=56-114
-
|notes=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].
+
|notes= '''UPDATE''' May 2008: Jesse has [http://www.ccs.neu.edu/home/tov/session-types/ a new implementation] 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].
For STM, see [http://web.mit.edu/price/a/2007/haskell/stm-long-intro-spj.pdf Simon Peyton Jones' gentle introduction],
For STM, see [http://web.mit.edu/price/a/2007/haskell/stm-long-intro-spj.pdf Simon Peyton Jones' gentle introduction],
or [http://web.mit.edu/price/a/2007/haskell/stm-lock-free-data-structures.pdf a paper applying STM to lock-free data structures].
or [http://web.mit.edu/price/a/2007/haskell/stm-lock-free-data-structures.pdf a paper applying STM to lock-free data structures].
-
For protocol/session types, see [http://scholar.google.com/scholar?q=%22session+types%22 the literature], or check out [http://okmij.org/ftp/Haskell/types.html 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 [http://www.ccs.neu.edu/home/tov/ Jesse's web page] to see if he's put up a paper or a new version.
+
For protocol/session types, see [http://scholar.google.com/scholar?q=%22session+types%22 the literature], or check out [http://okmij.org/ftp/Haskell/types.html 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 [http://www.ccs.neu.edu/home/tov/ 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 [http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html 1989 and later writeups].
For "theorems for free", see Phil Wadler's [http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html 1989 and later writeups].

Revision as of 07:46, 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 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