Lecture Materials
The course material is organized into 26 "lectures" plus a Caml programming tutorial, with slides (pdf) and other materials linked to below. Because I do not have corresponding reading notes, instructors will likely want enough expertise to know most of the content already. They will also surely want to modify/reorder/add/delete content, so below the list of lectures are all the source materials, instructions for using them, and a graph that approximates dependencies among lectures.
I use these materials in a 10-week (quarter, not semester) course with 2 80-minute lectures per week. Many lectures do not correspond to 80 minutes: Lectures 1, 2, 12, 17, 18, 19, 24, 25, 26, and possibly others are shorter; some others are likely longer. Overall there is more material than I can cover in 10 weeks, so I usually skip some or all of the material in lectures 13, 14, 18, 19, 25, and 26. Conversely, there may be too little material for a semester, but there are many great topics for which I have not developed materials, such as type inference, modules, programming with laziness, monads, type classes, denotational semantics (cf. lecture 5), Hoare logic, abstract interpretation, pi calculus, etc.
Slides and Other Materials
- 0. Caml Tutorial 1up-slides 6up-slides code (tar) (I do the tutorial between the material in Lectures 1 and 2)
- 1. Introduction 1up-slides 6up-slides
- 2. Syntax 1up-slides 6up-slides proofs
- 3. Operational Semantics 1up-slides 6up-slides handout proofs
- 4. Proofs about Operational Semantics 1up-slides 6up-slides proofs
- 5. Pseudo-Denotational Semantics 1up-slides 6up-slides code (.tar)
- 6. Little Trusted Languages; Equivalence 1up-slides 6up-slides proofs
- 7. Lambda Calculus 1up-slides 6up-slides
- 8. Reduction Strategies; Substitution 1up-slides 6up-slides
- 9. Simply Typed Lambda Calculus 1up-slides 6up-slides
- 10. Type-Safety Proof 1up-slides 6up-slides proofs
- 11. STLC Extensions and Related Topics 1up-slides 6up-slides
- 12. The Curry-Howard Isomorphism 1up-slides 6up-slides handout
- 13. Evaluation Contexts; 1st-Class Continuations; Continuation-Passing Style 1up-slides 6up-slides code (ml)
- 14. Efficient Lambda Interpreters 1up-slides 6up-slides code (ml)
- 15. Subtyping 1up-slides 6up-slides
- 16. Parametric Polymorphism 1up-slides 6up-slides
- 17. Recursive Types 1up-slides 6up-slides
- 18. Existential Types 1up-slides 6up-slides code (ml)
- 19. Type-and-Effect Systems 1up-slides 6up-slides
- 20. Shared-Memory Parallelism and Concurrency 1up-slides 6up-slides code (ml)
- 21. Synchronous Message-Passing and Concurrent ML 1up-slides 6up-slides code (ml) code (mli)
- 22. Class-Based Object-Oriented Programming 1up-slides 6up-slides
- 23. Types for OOP; Static Overloading and Multimethods 1up-slides 6up-slides
- 24. Bounded Polymorphism 1up-slides 6up-slides
- 25. Multiple Inheritance and Interfaces 1up-slides 6up-slides
- 26. Classless OOP 1up-slides 6up-slides
- 27. Higher-Order Polymorphism contributed by Matthew Fluet 1up-slides 6up-slides
Lecture Dependencies
(Caml tutorial and what depends on it not shown)
Source and Instructions for Editing the Materials
gpl_lecture_sources.tar contains all the files, mostly LaTeX, needed to produce the pdf files above. You need the LaTeX Beamer class (not included, but widely deployed) and mathpartir.sty (included for convenience).Instructions for editing and compiling lecture slides (nothing very complicated):
- Compiling is straightforward enough that I do not have a Makefile. If you have trouble, do not hesitate to ask.
- There are two
.texfiles that every lecture's.texfile includes (via\input):-
lecture_defs.texdefines macros for things like the title and instructor of the course. Edit this once to affect all lectures' title slides and footers. It also has basic Beamer configuration that you do not need to change unless you prefer different styles. -
lang_defs.texdefines macros relevant to PL semantics that are used in more than one lecture.
-
- Some slides use Beamer's
\pausecommand so that material appears incrementally, i.e., a very simple form of animation. By default, runningpdflatexwill cause each incremental version to appear on its own slide, as you want for presentation. Conversely, the documentclass optionhandoutrenders\pauseirrelevant so there is only one slide with all the content. At the top of each lecture's.texfile are two lines, one commented out, for easily toggling this behavior. - The 1up pdf files above were made without the
handoutoption. The 6up pdf files above were made with thehandoutoption followed by using Adobe Acrobat to "print" the file using these non-standard options: landscape orientation, 6-pages per sheet, fit to printable area. While there are command-line tools to automate printing 6-up, I have not found their output as visually pleasing.
