15-814 Types and Programming Languages
| Fall 2021 |
| Frank Pfenning |
| Tue Thu 10:10-11:30 ET |
| GHC 4301, In-Person Expectation (IPE) |
| 12 units |
| First lecture will be Tue Aug 31 |
This graduate course provides an introduction to programming languages viewed
through the lens of their type structure.
Prerequisites: This is an introductory graduate course with
no formal prerequisites, but an exposure to various forms of mathematical
induction will be helpful. 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.
Class Material
| Schedule |
Lecture notes and additional readings
|
| Assignments |
Homework assignments and due dates |
| Resources |
Policy details and links to other resources |
| Software |
Software in support of the course |
Course Information
| Lectures |
Tue Thu 10:10-11:30, GHC 4301 |
| Instructor |
Frank Pfenning, fp@cs
Office Hour Mon 11:00-12:00, GHC 6017
Zoom Office Hour TBA
|
| Teaching Assistant |
David Kahn, davidkah@andrew
Office Hour Wed 11:00-12:00, GHC 6503
|
| Course Communication |
piazza.com/cmu/fall2021/15814/home |
| Lectures Notes |
Lectures notes will be posted on the schedule page,
within a day or two after of the lecture
|
| Textbook (optional) |
Robert Harper,
Practical Foundations for Programming Languages (Second Edition),
Cambridge University Press, April 2016.
|
| Credit |
12 units |
| Grading |
600 pts homework, 150 pts midterm exam, 250 pts final mini-project |
| Homework |
Homework assignments are posted on the assignments page
Homework submission is on Gradescope
|
| Midterm |
The midterm exam is in lecture (80 minutes), closed book, closed notes
|
| Final |
The final exam is replaced by a Mini-Project
|
| Home |
http://www.cs.cmu.edu/~fp/courses/15814-f21/ |
Learning objectives:
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
Core 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
Prior Versions of This Course
[ Home
| Schedule
| Assignments
| Resources
| Software
| Software
]
fp@cs
Frank Pfenning
|