PLATYPUS
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.
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).
Content
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.
Agenda
For details on what we've covered and what we'll be reading next see the Meetup group
Resources
The online Type Theory Study Group
- Type Theory Study Group on Google Groups
- ##typetheory on Freenode.net IRC
- @type_theory on Twitter
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