The study group has seemed to have died out quite a bit, unfortunately. I've been thinking that part of the reason for this could be a lack of sufficiently clear objectives for the study group, and potential confusion over how the PFPL book in particular fits into this picture.
I've free-writed a statement about what the 'official' objectives of the group possibly could be, and made a sharpened list of topics to study to meet theses objectives, aligned with PFPL in part. Open to suggestions; just something I felt like writing down and wanted to share, to see how it would fit from other participant's perspectives and goals. Thoughts?
---
The objective of the Type Theory Study Group is to foster an online community, open to all, dedicated to learning type theory. As a study group, one of our aims is to break the entire body of literature on type theory considered into smaller parts, and collectively learn each individual part in an appropriate ordered fashion. To learn each part of the literature on type theory, we wish to organize online group discussions dedicated to disseminating and offering exercises on said part of the literature, to focus on gaining an understanding of it. Type theory is arguably quite an interesting subject area, with interesting connections and applications to programming language theory, computational linguistics, formalized mathematics, and more recently, synthetic homotopy theory; however, it is seemingly difficult to find pedagogical materials on type theory organized in an appropriately clear and centralized fashion. Ultimately, we hope to solve the problem of this experienced high barrier-to-entry to type theory - and hope that everybody gives and takes something away from the study group that will help them achieve goals in their respective disciplines.
Thus far we have formally organized a few Google hangouts to discuss the metatheoretical prerequisities necessary to study type theory. However, we are now looking for more volunteers, and are interested in moving forward. Please post on the mailing list if you are interested in volunteering: anyone is welcome and encouraged to lead or join a discussion!
Here is a proposed list of subparts of the literature to study:
- Lambda calculus, abstract binding trees, logical frameworks, and metatheorical preliminaries.
- Intuitionistic logic, simple type theory, Heyting algebras, and cartesian closed categories.
- Propositions as types, proofs as programs, and formal dependently-typed lambda calculi.
- System F (in the context of programming languages), type-safety, and parametricity.
- Finite data types, infinite data types, and the bar induction principle.
- Linear type theory, game semantics and vector space semantics.
- Set-theoretic perspectives on type theories, types as generalized topological spaces, and elementary topos theory.
- Dana Scott's logic for computable functions, denonational semantics and meaning theory.
- Proof refinement logics, computational type theories, and interesting proofs in open-ended computation systems.
- Homotopy-theoretic models of type theory, higher type theory, and achieving Alexander Grothendieck's goal for a formal axiomatic theory of infinity groupoids (in the context of doing homotopy theory synthetically).
---
Thanks,
Mark
