Lunchtime type theory study group in Sydney
Switch branches/tags
Nothing to show
Clone or download
Pull request Compare This branch is 20 commits ahead, 107 commits behind type-theory:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.


Type Theory Study Group

PLATYPUS* is a study group meeting weekly in Sydney, Australia for people interested in learning more about type theory and its connections to programming languages.

Gitter chat
Twitter @SydneyTypes
Meetup Sydney Type Theory

All are welcome!

Inspired by the online Type Theory Study Group 2015.

* Programming Languages and Types (yet perfectly understandable) in Sydney — thanks to Danny Gratzer for the name suggestion.

When and where

We meet on Monday lunchtimes from 12:30 to 2:00 pm.

Venue is the Commonwealth Bank of Australia, 255 Pitt Street Sydney.

Please RSVP via the Meetup page for catering purposes (and let us know if you have any particular dietary requirements).


During 2015 and 2016 we read Bob Harper's Practical Foundations of Programming Languages, 2nd Edition.

In 2017 we're reading Simon Thompson's Type Theory and Functional Programming.


For details on what we've covered and what we'll be reading next see the Meetup group


The online Type Theory Study Group

Other resources

  • learn-tt is a great collection of resources for learning type theory.

Proposed Future Topics

  • The Untyped Lambda Calculus / Operational Semantics
  • The Simply Typed Lambda Calculus / Progress and Preservation
  • Propositions as Types / Proofs as Programs
  • System F / Parametricity
  • Martin-Löf's Extensional Type Theory / Constructive Mathematics and Computer Programming
  • Identity Types / Proofs of Equality in Martin-Löf's Intensional Type Theory
  • Topological Spaces as Types / Points as Programs
  • Intensional Proofs of Equality as Paths between Spaces
  • Proofs of Equality of Equalities as Synthetic Homotopies
  • Homotopy Type Theory / Higher Inductive Types / Univalence
  • Canonicity for Homotopy Type Theory / Current Issues
  • Special Cases of Homotopy Type Theory with Canonicity / Cubical Type Theories
  • Martin-Löf's (Equational) Logical Framework and the Monomorphic Theory of Sets
  • The Edinburgh Logical Framework / "Mechanizing Metatheory in a Logical Framework"
  • Categorical Semantics of Type Theories / Connection to Category Theory Study Group