Literature

We collect here some interesting literature you can take a look at. This list will grow as the course continues.

  • Girard, “Proofs and Types”, PDF here
  • Wadler, “Theorems for Free”, PDF here
  • Reynolds, “Types, Abstraction, and Parametric Polymorphism”, PDF here
  • Mitchell and Plotkin, “Abstract types have existential type”, PDF here
  • Cardelli and Leroy, “Abstract types and the dot notation”, PDF here
  • Harper, Mitchell, Moggi, “Higher-Order Modules and the Phase Distinction”, PDF here
  • MacQueen, “Using Dependent Types to Express Modular Structure”, PDF here
  • Rossberg, Russo, Dreyer, “F-ing Modules”, PDF here
  • Pitts and Stark, “Operational Reasoning for Functions with Local State”, PDF here
  • Reynolds, “Separation Logic: A Logic for Shared Mutable Data Structures”, PDF here
  • Pfenning and Davies, “A Judgmental Reconstruction of Modal Logic”, PDF here
  • Appel et al., “A very modal model of a modern, major, general type system”, PDF here
Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.