Abstracts.2020.STLC&Subtyping

Subtyping and Bidirectional Type Checking in STLC

by Sandro Stucki

Abstract

(TBA)

Resources

(TBA)

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.