What we're about

Let's get together and learn about type theory!

We're a type theory reading group in Sydney, Australia. Inspired by the online type theory study group (https://github.com/type-theory/type-theory-study-group-2015), our focus is type theory with a view towards programming languages.

We're currently reading Simon Thompson's Type Theory and Functional Programming (https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/).

In the past we read much of Bob Harper's "Practical Foundations for Programming Languages", 2nd Edition (http://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf), with some excursions into other topics, including modal type theory and linear types, as well as implementations in Twelf and Idris. Our resident expert is Rowan Davies (http://www.cs.cmu.edu/~rowan/).

Some videos of past sessions are available via the following link, including two catch up sessions (highly recommended for new members):

https://www.youtube.com/channel/UCvF2Txs3F-... (https://www.youtube.com/channel/UCvF2Txs3F-ZEXv7w_fCz-1Q)

Upcoming events (5+)

Homotopy Type Theory

Commonwealth Bank of Australia

We'll be reading "Homotopy Type Theory: Univalent Foundations of Mathematics" aka "The HoTT Book". https://homotopytypetheory.org/book/ We'll start with Chapter 1, which provides an overview of Martin-Löf type theory, but from the perspective of homotopy type theory.

Homotopy Type Theory

Commonwealth Bank of Australia

We'll be reading "Homotopy Type Theory: Univalent Foundations of Mathematics" aka "The HoTT Book". https://homotopytypetheory.org/book/ We'll start with Chapter 1, which provides an overview of Martin-Löf type theory, but from the perspective of homotopy type theory.

Homotopy Type Theory

Commonwealth Bank of Australia

We'll be reading "Homotopy Type Theory: Univalent Foundations of Mathematics" aka "The HoTT Book". https://homotopytypetheory.org/book/ We'll start with Chapter 1, which provides an overview of Martin-Löf type theory, but from the perspective of homotopy type theory.

Homotopy Type Theory

Commonwealth Bank of Australia

We'll be reading "Homotopy Type Theory: Univalent Foundations of Mathematics" aka "The HoTT Book". https://homotopytypetheory.org/book/ We'll start with Chapter 1, which provides an overview of Martin-Löf type theory, but from the perspective of homotopy type theory.

Past events (176)

Homotopy Type Theory

Commonwealth Bank of Australia

Photos (10)