Types and Programming Languages

Course ID 15814

Doctoral Breadth Course: Programming Languages - (*)
Classes marked with "*" (star) are appropriate for any CSD doctoral or 5th year master's student.

Description

The course studies the theory of type systems, with a focus on applications of type systems to practical programming languages. The emphasis is on the mathematical foundations underlying type systems and operational semantics. The course includes a broad survey of the components that make up existing type systems, and also teaches the methodology behind the design of new type systems.

Key Topics
Static and dynamic semantics
Preservation and progress
Hypothetical judgments and substitution
Propositions as types, natural deduction, sequent calculus
The untyped lambda-calculus
Functions, eager and lazy products, sums
Recursive types
Parametric polymorphism, data abstraction, existential types
K machine, S machine, substructural operational semantics
Shared-memory concurrency, session types

Required Background Knowledge
This is an introductory graduate course with no formal prerequisites, but an exposure to various forms of mathematical induction will be helpful.

Course Relevance
Enterprising undergraduates and masters students are welcome to attend this course. If you have already taken 15-312 Principles of Programming Languages at CMU, please check with the instructor if this course is suitable for you.

Course Goals
After taking this course, students will be able to

define programming languages via their type system and operational semantics
draw from a rich set of type constructors to capture essential properties of computational phenomena
state and prove the preservation and progress theorems or exhibit counterexamples
recognize and avoid common fallacies in proofs and language design
write small programs to illustrate the expressive power and limitations of a variety of type constructors
state and prove properties of individual programs based on their semantics or exhibit counterexamples
critique programming languages and language constructs based on the mathematical properties they may or may not satisfy
appreciate the deep philosophical and mathematical underpinnings of programming language design