Instructor: Cormac
Flanagan
Office: Engineering 2 Building, room 271
Office Hours: After class, and by
appointment
Class: TuTh 2-3:45pm, SE lab, E2-292
This course is intended to provide students
with foundational knowledge about type systems and their use in programming
languages. The study of type systems is an exciting and deep field, with
important applications to software reliability, performance, security, code
mobility, and with significant impacts on programmer productivity and software
engineering. Key topics will include
type safety, type reconstruction, polymorphism, subtyping, constraint types,
and the practicality of various approaches.
Textbook: Types and Programming
Languages, Benjamin C. Pierce.
One copy will be made available in the Software Engineering lab, E2-393.
One copy is on 2-hour reserve at the Science Library.
CMPS203
Programming Languages, or a similarly semantics-oriented course in programming
languages.
1. Class Participation (30% of total grade)
Discussions will be
a key part of the class learning experience, and will help you internalize the
technical material and understand important connections. Students are expected
to (a) complete and take notes on assigned readings before attending class, (b)
arrive punctually, and (c) engage actively in class discussions. In this class
we will all share responsibility for teaching and learning.
2. Class Presentations (20% of total grade)
Each student will
give oral presentations during class on a particular topic, mostly chosen from
the textbook. These presentations should
highlight the key points – main definitions, theorems, properties, design
choices, etc – and should include clear motivation for the topic. Either
blackboard or powerpoint presentations are acceptable. Students are encouraged to
engage the audience as much as possible, by asking questions and inciting
discussion. Each class will consist of one student presentation on a particular
topic, followed by (or preferably co-mingled with) a discussion of that topic.
3. Presentation Buddy (5% of total grade)
Each student
presenter will be helped by a corresponding “buddy”, who will
listen to and provide constructive feedback on a trial run of the presentation,
with the goal of improving the classroom presentation. (You might find two trial
runs, one short and one a bit longer, to be helpful.) The buddy grade will
correspond to the grade for the resulting classroom presentation.
4. Scribe (10% of total grade)
The
“buddy” for each presentation will also function as a
“scribe” who documents the classroom discussion. This write-up
should not be a repetition of the corresponding book chapters, but an addendum
that documents the key insights of the discussion and emphasizes the key
points. It should be 2-5 pages long and be emailed to the Professor before the
next class for posting on the web page.
5. Homework (15% of total grade)
Homeworks will be
assigned during the quarter, and are expected to be completed on time, before
the start of the class when they are due. Late homeworks will be deducted 10%
for each day (or fraction of day) late.
6. Project (20% of total grade)
Students will
complete a class project, either individually or in pairs. The project should
be an implementation of some type system, preferably somewhat different from
the type systems in the book, and perhaps applied in a different context or to
a different language. Working with a small idealized language is recommended,
due to time constraints. Each project will include a 20 minute presentation,
sometime in the last two weeks of the quarter.
Some possible ideas for projects include:
·
An
implementation that works with and preserves typing derivations while
transforming code, much like TAL (typed assembly language). A (much too simple)
example would be desugaring “;”.
A few steps up from there might yield an interesting project.
·
Implement
a “refactoring” for featherweight Java. Refactoring to introduce
“most-general types” might be good. Refactoring to introduce
generic (Java 5) types might be harder.
·
Kenn
expressed interest in Generalized Algebraic Data Types
·
Constraint-based
type inference for Subtyping
·
Information
flow analyses
·
Ownership
types
·
Dependent
types
·
Exploring
Twelf
·
You
could take some type system for a lambda-calculus-like language and port it to
a different langage, perhaps some dialect of Prolog or a class-based OO
language.
Date
|
Topic
|
|
Presenter
|
Scribe
|
HW
Due
|
|
3/29 |
Introduction, administrivia |
|
Cormac |
- |
|
|
3/31 |
Background |
Ch. 1-7 |
Cormac |
- |
3.5.10, 3.5.13, 5.3.8 |
|
4/5 |
Simply-Typed Lambda Calculus
|
Ch. 8-10 |
Jessica |
Avik (pdf) |
8.2.3, 8.3.{6-8}, 9.2.3, 9.3.2, 9.3.10 |
|
4/7 |
--- no class --- |
|
|
|
|
|
4/12 |
Extensions |
|
Karl |
Pritam (pdf) |
|
|
4/14 |
References and Exceptions |
|
Mark |
Aaron (pdf) |
Extend ch10 with eg fix |
|
4/19 |
... continued ... |
same |
same |
same |
15.2.4, 15.5.{2-3} |
|
4/21 |
Subtyping |
|
Pritam |
Karl (pdf) |
None |
|
4/26 |
Imperative Objects |
|
Cormac |
Cormac |
None |
|
4/28 |
Featherweight Java |
|
Kenn |
Mark (pdf) |
None |
|
5/3 |
Recursive Types |
|
Aaron |
Sean (pdf) |
Implement |
|
5/5 |
Universal, Existential Types |
|
Avik |
Jessica (pdf) |
|
|
5/10 |
... continued ... |
same |
Avik |
Jessica (pdf) |
|
|
5/12 |
Type Reconstruction |
Ch.22 |
Sean |
Kenn |
|
|
5/17 |
|
|
|
|
|
|
5/19 |
Bounded quantification Metatheory of bdd quantific. |
Ch.26 Ch.28 |
Jessica Karl |
Avik (pdf) Pritam |
|
|
5/24 |
TBD |
|
|
||
|
5/26 |
Type Operators |
Ch.29 |
Aaron |
Sean |
|
|
5/31 |
Higher-Order Polymorphism & project
presentations |
Ch.30 |
Kenn |
Mark (pdf) |
|
|
6/2 |
Higher-Order Subtyping & project presentations |
Ch.31 |
Pritam |
Karl (pdf) |
|
Note: This schedule is tentative, and may change as the quarter progresses.
Additional homeworks will be announced during the quarter. Students will sign
up for presentation/scribe slots during the first week of the quarter. We may
also have guest speakers on some advanced topics. Towards the end of the
quarter we may cover additional topics, perhaps including:
·
Constraint-based
type inference for Subtyping
·
Information
flow analyses
·
Typed assembly
language
·
Refactoring
for generics in Java
·
Ownership
types
·
Dependent
types