Semantics

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