Type Systems for Modules (Winter 2010)


Course Information

Lecture type: Seminar, 7 CPs (?)
Time: Mon, 4-6pm
Room: MPI-SWS (Wartburg) in 304
Instructor: Derek Dreyer

Description

Module systems are central to the construction of large-scale programs, and there is a rich and highly-developed theory devoted to the study of type systems for modules. In this seminar course, we will focus attention on the origins, design, semantics and implementation of the ML module system, one of the most influential and highly evolved module systems available. We will investigate the numerous issues that arise in formalizing ML modules, as well as the different styles of formalization (e.g. ad-hoc, direct-style, elaboration), and we will also study a variety of challenging extensions to the ML module system, including higher-order functors and recursive modules.

There will be one 2-hour lecture per week. Students will be expected to read 1-2 papers per week and to participate in a lively class discussion. There will also be a relatively lightweight class project (e.g. writing a short survey paper or preparing a lecture on advanced material, implementing an advanced module system design). The course is taught in English, and is intended for students who have already taken a course in semantics and/or type systems for programming languages.

Schedule

Date Description / Reading Leader,
Questions
Scribe,
Notes
Mon, Oct 18
Introduction to the seminar.
Mon, Oct 25
Using types to describe modules. Scott
txt link
Scott
pdf link
Tue, Nov 2
12:15 to 2:00
Manifest types and translucent signatures. Beta
txt link
Scott
pdf link
Mon, Nov 8
12:15 to 2:00
Module type systems based on System F.
Auxiliary reading:
Jonas
txt link
Sigurd
pdf link
Mon, Nov 15
More on functors. Only read Chapter 1 of Dreyer's thesis. Sigurd
txt link
Beta
(none yet)
Mon, Nov 22
Unified framework for both generative and applicative functors. Keep working on last week's questions, too. Derek
(none yet)
Jonas
(none yet)
Wed, Dec 1
6:15 to 8:00
Classifications of modules by purity. Continuation of Dreyer's thesis (Chapter 2). Derek
txt link
Jonas
(none yet)
Mon, Dec 6
Recursive modules are harder than you think. Bring the auxiliary papers to class with you, whether you read them or not.
Auxiliary reading:
Derek
(none yet)
Georg
pdf link
Mon, Dec 13
You can skip most of the metatheory details for now (Section 4), and focus on the other sections. Derek
(none yet)
Gil
(none yet)
Mon, Jan 3
Recap and question time.
Mon, Jan 10
More on recursive modules.
(none yet)

(none yet)
Mon, Jan 17
12:15 to 2:00
Mixin modules. Only read Sections 1-3 of the MixML paper. Print out and take a quick look at the Owens and Flatt paper, too.
Auxiliary reading:

(none yet)

(none yet)
Mon, Jan 24
cancelled
Cancelled due to POPL conference.
Wed, Feb 2
6:15 to 8:00
MixML.
(none yet)

(none yet)
Mon, Feb 7
Finish discussing MixML.
(none yet)

(none yet)

Likely Topics for the Seminar


Last modified: July 03 2012 17:36:03