I haven't read Wadler's paper, so he may well refer to this, but he relation between programs and proofs generally falls under the well-known Curry--Howard Corr

I haven't read Wadler's paper, so he may well refer to this, but he relation between programs and proofs generally falls under the well-known Curry--Howard Correspondence[1], Curry being, of course, Haskell Curry, namesake of the language and the practice of Currying. [1]http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...