Course Description and Requirements
Static and dynamic typing offer complementary advantages: static
typing (as in Java, C#, or ML) provides early error detection,
efficient execution, and better documentation of code, whereas
dynamic typing (as in various scripting languages) encourages
rapid development and makes it easier to adapt to changing
requirements. Traditionally, programming languages have
supported either static or dynamic typing, but not both. Over
the last decade there has been a flurry of research on
gradual type systems that allow statically checked and
dynamically checked components to be freely mixed. Another
kind of mixing happens in
multi-language software systems
which are assembled using components written in different
programming languages --- statically typed and dynamically
typed, high-level and low-level. Formally reasoning about how
components from such different languages should interoperate
becomes essential when verifying
correct compilation of
components that may be linked with code compiled from
other languages. This course seeks to cover this spectrum of
interconnected issues.
Topics include:
- Type systems: simple types, polymorphism and parametricity,
substructural types, dependent types
- Gradual typing, contracts, blame tracking, refinement
types, multi-language interoperability, manifest contracts, and hybrid typing
- A brief look at space-efficiency issues in contracts
- Compilation: type-preserving compilers, compiler correctness, and
security-preserving compilation
The course is a research seminar that primarily focuses on
reading and discussing papers from the scientific literature.
The instructor will cover the basic vocabulary and techniques
associated with type systems during the first three weeks.
After that, at each class meeting, a student will be responsible
for presenting a research paper. All students will be required
to read the paper, submit a short critique of the paper before
class, and come to class prepared to discuss the reading in depth.
This course is intended primarily for PhD students; however, MS
students and as well as advanced undergraduates as
welcome. Familiarity with programming language semantics and
type systems (as covered in cs5400 or cs7400), or a willingness
to pick up the material --- see
background reading notes below
--- is required, since most of the readings
assume basic familiarity with these. If you are a first or
second year Ph.D student interested in taking this course, but
you have not yet taken cs7400 (IPPL), I would nonetheless
encourage you to take this class as it will only be offered this
once.
Prerequisites
CS 5400 (PPL) or CS 7400 (Intensive PPL).
Textbooks
Readings will include a few chapters from the following books:
Grading
Students will be evaluated on the basis of
- two homework assignments on the core topics covered in the
first three weeks of the course (10%)
- one (or two) in-class presentations of research papers,
along with lecture notes on the presentation that will be
distributed to the class (40%)
- participation in class discussion (20%)
- written critiques of papers (30%) (Note: you have 4
free passes over the course of the semester; that is, you can
you can choose not to submit a critique for up
to 4 papers during the course of the semester without it
affecting your grade.)
To pick up the background material required for this course you
should read
one of the following:
- The following chapters from Pierce'sTypes
and Programming Languages (TAPL): start with chapters 1-3, 5-6,
8-9, 11, 13, and 14. (Provides a gradual introduction to the
material and the first few chapters are a really quick read.)
- Cardelli's Type
Systems. (Assumes prior exposure to basic
techniques from the formal study of programming languages.)
Auditing
Auditors are welcome. Auditors will be expected to do the
readings, submit critiques, and participate in class discussion.
Talk to the instructor if you want to audit the course.