Curry-Howard seminar

Fri, Jul 15, 2016

This is the webpage for the Curry-Howard seminar at the University of Melbourne, which is on Tuesdays from 2-3pm in Room 107 of Richard Berry. The seminar has as its theme the growing field of connections between logic, functional programming and category theory, sometimes referred to as the Curry-Howard correspondence (or by the slogan “formulas-as-types, proofs-as-programs”). To receive announcements about the seminar subscribe to the mailing list. You should also check out the Logic Seminar which has talks on more recent research in logic.

Our aim is to read Sorensen and Urzyczyn’s book “Lectures on the Curry-Howard isomorphism”, up to the proof of the original Curry-Howard correspondence (between simply-typed lambda calculus and intuitionistic logic) in Chapter 4, and to augment this with a third equivalence which involves category theory.

Schedule

  • 14-7 William Troiani “The Church-Rosser Theorem” (lecture notes)
  • 2-8 William Troiani “Introduction to lambda calculus” (Sections 1.1-1.3, lecture notes)
  • 9-8 Samuel Lyons “All partial recursive functions are lambda-definable” (Section 1.7, lecture notes)
  • 16-8 James Clift “Simply-typed lambda calculus and strong normalisation” (Chapter 3, lecture notes)
  • 23-8 Shawn Standefer “Introduction to natural deduction” (Chapter 2, lecture notes)
  • 30-8 Daniel Murfet “The category of simply-typed lambda terms” (lecture notes)
  • 6-9 Shawn Standefer “Kripke semantics of intuitionistic logic” (lecture notes)
  • 13-9 No talk, instead we’ll watch Wadler’s Propositions as types and discuss
  • 20-9 Daniel Murfet “The category of simply-typed lambda terms II” (lecture notes and an appendix)
  • 4-10 Daniel Murfet “The Curry-Howard principle” (lecture notes)
  • 11-10 James Clift “System F: Polymorphic lambda calculus” (lecture notes)
  • 18-10 William Troiani “System F in the real world: Haskell and functional programming” (lecture notes) (the referenced talk by Rich Hickey is “Simple made easy”)

References

For the more categorical aspects, see:

  • Taylor “Practical foundations for mathematics”
  • Lambek, Scott “Introduction to higher-order categorical logic”
  • Barr, Wells “Toposes, triples and theories”
  • Lawvere “Equality in hyperdoctrines and comprehension schema as an adjoint functor”

Other

  • The functional programming language Haskell compiles to an extension of System F. There was a recent blog post by Stephen Diehl on this, and a talk by Simon Peyton Jones.

  • An interesting podcast on Type Theory.

  • Videos from the ICFP 2016 functional programming conference.

  • Videos from a recent functional programming conference Compose in Melbourne.

  • Video of Yann LeCun on Deep Learning and the Future of AI. Perhaps there is a missing differentiable column in the Curry-Howard correspondence. From 49:30 of the video: “Analogy through algebra: this is very important because a lot of us have been thinking that reasoning should not be done through logic or rules, but should be done through continuous mathematics. And the reason for that is that instead of symbols you have vectors, instead of logical operations you have continuous mathematical operations like linear algebra. The reason for doing is that is that now every operation the machine does is differentiable, so you can train it to do reasoning.” (see 55:00 for memory).