Mon, Mar 19, 2018

The seminar is on Wednesdays from 3-4:30pm in Room 107 of Peter Hall. For announcements of talks subscribe to the mailing list. The videos from the talks are available on Vimeo and YouTube. 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:

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.

Talk schedule:


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

Previous semesters of the seminar

S2 2016 - Curry-Howard correspondence

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


S2 2016 - Topological field theory

Our aim was to read Kock’s book on the equivalence between closed 2D TFTs and commutative Frobenius algebras. The talks:

  • 28-7 Daniel Murfet “Topological Quantum Field Theory in two dimensions” (slides).
  • 4-8 Patrick Elliott “Introduction to Frobenius algebras” (lecture notes).
  • 11-8 Michelle Strumila “The cobordism category 2Cob” (beginning of Chapter 1, lecture notes).
  • 18-8 Omar Foda “Supersymmetry and Morse theory” (references are Witten’s paper and Nicolas Mee’s thesis).
  • 1-9 Patrick Elliott “The category of Frobenius algebras” (lecture notes).
  • 8-9 Thomas Quella “Chern-Simons theory as an example of a TQFT” (lecture notes).
  • 15-9 Campbell Wheeler “Symmetric monoidal categories and functors” (lecture notes).
  • 13-10 Daniel Murfet “The cobordism category” (lecture notes).