This is the webpage for the Curry-Howard seminar, which is about logic, categories and computation. The seminar is on **Thursdays from 2-3pm** in Room 107 of Peter Hall at the University of Melbourne. For announcements you can subscribe to the mailing list, follow the seminar on Twitter, or see all the videos on our vimeo channel. For previous semesters of the seminar, scroll down!

Our aim this semester is to understand how to use adjoint functors and topoi to organise mathematical knowledge, following Mac Lane and Moerdijk’s book “Sheaves in Geometry and Logic”. For an explanation of this aim see the seminar announcement and the first lecture below. For some additional motivation, see:

- Caramello’s paper “The unification of mathematics via topos theory”,
- Cartier’s paper “A mad day’s work: from Grothendieck to Connes and Kontsevich”,
- Higher topoi are important in homotopy type theory,
- Connes’ talk on “The arithmetic site”.

The seminar is supported by funding from Data61, DST group and ACEMS as part of a collaboration which aims to develop new tools to aid human reasoning about mathematics and software.

- 8-3 Daniel Murfet “An invitation to topos theory” (lecture notes | video)
- 15-3 Daniel Murfet “The Curry-Howard correspondence (Part 1)” (lecture notes | video | more notes | response to Sam’s question)
- 22-3 Will Troiani “Monads and programs” (lecture notes | video)
- 29-3 James Clift “The definition of a topos (Part 1)” (lecture notes | video)
- 5-4
**No talk** - 12-4 James Clift “The definition of a topos (Part 2)” (lecture notes | video)
- 19-4 Patrick Elliott “Sheaves of sets (Part 1)” (lecture notes | video)
- 26-4 Patrick Elliott “Sheaves of sets (Part 2)” (lecture notes | video)
- 10-5 Will Troiani “Higher-order logic and topoi (Part 1)” (lecture notes | video)
- 21-6 Daniel Murfet “Higher-order logic and topoi (Part 2)” (lecture notes)
- 28-6 Patrick Elliott “Sheaves form a topos (Part 1)”
- 5-7 Daniel Murfet “Higher-order logic and topoi (Part 3)”
- 12-7 Patrick Elliott “Sheaves form a topos (Part 2)”
- 19-7 Daniel Murfet “Classifying topoi (Part 1)”
- 26-7 Daniel Murfet “CLassifying topoi (Part 2)”

- Mac lane, Moerdijk “Sheaves in Geometry and Logic”.
- Lambek, Scott “Introduction to higher-order categorical logic”
- Barr, Wells “Toposes, triples and theories”
- Sorensen, Urzyczyn “Lectures on the Curry-Howard isomorphism”.

Our aim was 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.

- 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”)

The references:

- Sorensen, Urzyczyn “Lectures on the Curry-Howard isomorphism”.
- Girard, Lafont, Taylor “Proofs and types”.
- Gallier “Constructive Logics Part I”.
- Wadler “Propositions as types”.
- Martin-Lof “On the meanings of the logical constants and the justifications of the logical laws”.

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”

- 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.