Slides for Lecture 2

Slides for Lecture 3

Slides for Lecture 4

Types, Abstraction and Parametric Polymorphism. John C. Reynolds. Information Processing 83 (1983), pp. 513-523. [pdf]

Theorems for Free! Philip Wadler. Proceedings, Functional Programming Languages and Computer Architecture 1989 (FPCA'89), pp. 347-359. [pdf]

Computing Left Kan Extensions. M. R. Bush, M. Leeming, and R. F. C. Walters. Journal of Symbolic Computation 35 (2003), pp. 107-126. [pdf]

GADTs, Functoriality, Parametricity: Pick Two. Patricia Johann, Enrico Ghiorzi, and Daniel Jeffries. Accepted for presentation at Logical and Semantic Frameworks with Applications (LSFA'21). [pdf]

Parametricity for Primitive Nested Types. Patricia Johann, Enrico Ghiorzi, and Daniel Jeffries. Proceedings, Foundations of Software Science and Computation Structures 2021 (FoSSaCS'21), pp. 324-343. [pdf]

Deep Induction: Induction Rules for (Truly) Nested Types. Patricia Johann and Andrew Polonsky. Proceedings, Foundations of Software Science and Computation Structures 2020 (FoSSaCS'20), pp. 339-358. [pdf]

Higher-Kinded Data Types: Syntax and Semantics. Patricia Johann and Andrew Polonsky. Proceedings, Logic in Computer Science 2019 (LICS'19). [pdf]

Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08), pp. 297-308. [pdf]