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.
</br/>
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.
We meet on Wednesday lunchtimes from 12 noon to 1:30.
Venue is the Commonwealth Bank of Australia, 201 Sussex Street Sydney.
Please RSVP via the Meetup page for catering purposes (and let us know if you have any particular dietary requirements).
At the moment we're reading Bob Harper's Practical Foundations of Programming Languages, 2nd Edition.
- Wednesday 4 November Chapter 3: Hypothetical and general judgements
-
Wednesday 28 October
Discussed chapters 1 and 2 ("Abstract Syntax" and "Inductive definitions").
Introduction to Twelf.
-
Wednesday 21 October
General discussion of type theory, vote on name proposals.
- Type Theory Study Group on Google Groups
- ##typetheory on Freenode.net IRC
- @type_theory on Twitter
- learn-tt is a great collection of resources for learning type theory.
- 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