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 typing which allows statically typed and
dynamically typed 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 --- more precisely and less precisely
typed, high-level and low-level, and ones that support disparate
type features. When developers mix components written in different
programming languages, there is a question of how they
ought to
reason about the behavior of single-language components that will linked
with code from other languages with different expressive power, and a
question of how compiler and language design should evolve to make such
reasoning easier for developers. This course seeks to cover this spectrum
of interconnected issues.
Topics include:
- Type systems: simple types, polymorphism and parametricity,
mutable memory, substructural types, dependent types, session types
- Gradual typing, contracts, refinement types, multi-language interoperability, and hybrid typing
- Compilation and linking: 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 undergraduates are
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), or permission from instructor.
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. Also, you do not need to
submit critiques for papers you are presenting.)
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, and participate in class discussion. They are also
welcome to present a research paper.
Talk to the instructor if you want to audit the course.