-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2020.STLC&Subtyping
Sandro Stucki edited this page Dec 10, 2020
·
4 revisions
by Sandro Stucki
We roughly covered the following:
- syntax, typing and subtyping rules of STLC + Top & Bottom types + subtyping;
- how the presence of subtyping (in particular the subsumption rule) complicates the meta-theory of this calculus: illustrated via the example of subject reduction (which needs additional lemmas: generation for typing, subtyping inversion);
- a more algorithmic presentation: bidirectional type checking + subtyping;
- some sketches of how to interpret subtyping via coercions in a CCC.
The handwritten notes produced by Sandro during the lecture.
- Benjamin C. Pierce: Types and Programming Languages. 2002. This is the definitive guide to type systems. Chapters 15 Subtyping and 16 Metatheory of Subtyping in section III Subtyping are especially relevant.
- Wikipedia: Simply Typed Lambda Calculus. Section Alternative Syntaxes contains a short but intuitive presentation of bidirectional type checking.
- Conor McBride: I Got Plenty o' Nuttin'. 2016. This more advanced treatment of bidirectional type checking covers dependent types and much more. Also available from Conor's website here.