Abstracts.2020.STLC&Subtyping

Subtyping and Bidirectional Type Checking in STLC

by Sandro Stucki

Summary

We roughly covered the following:

• syntax, typing and subtyping rules of STLC (+ base type (b)) + top type (⊤) + bottom type (⊥) + subtyping relation (<:);
• how the presence of subtyping (specifically the subsumption rule) complicates the meta-theory of this calculus: illustrated via the example of the subject reduction property, which needs the additional "generation" and "subtyping inversion" lemmas;
• a more algorithmic presentation: bidirectional type checking + subtyping;
• some sketches of how to interpret subtyping via coercions in a CCC.

Resources

The handwritten notes produced by Sandro during the lecture.

References

1. 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.
2. Wikipedia: Simply Typed Lambda Calculus. Section Alternative Syntaxes contains a short but intuitive presentation of bidirectional type checking.
3. 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.