Frustrated with your current programming language? Ever wanted to create your own? This course teaches you the state of the art tools and techniques for defining programming languages and proving that they do what you want them to do. You will learn about type systems and operational semantics and how to use them to model modern programming language features such as objects and generics. You will come away knowing the fundamental principles common to most programming languages, making it much easier to learn new languages.
When: Spring 2010
Class times: 3:20-5:50pm Tuesdays
Where: ECEE 265
Textbooks:
- Types and Programming Languages by Benjamin C. Pierce
- Isabelle/HOL: A Proof Assistant for Higher-Order Logic
Office hours: TBA
Course outline (from 2008, the 2010 course will cover fewer topics but with more mathematical rigor):
- Introduction
- Mathematical Preliminaries (sets, induction, etc.)
- Untyped lambda calculus and operational semantics
- Simply-typed lambda calculus and type systems
- Type safety proofs
- Subtyping
- Featherweight Java
- Gradual type systems that mix static and dynamic typing
- Polymorphism: universal and existential types
- Type inference and ML
- Bounded quantification
- C++ constrained templates
- Higher-order type systems with type operators
- Type systems for metaprogramming and MetaML
Class Email Group For announcements and discussion. Please sign up ASAP!
Lecture Schedule:
- Lecture 1, Jan. 12: Grammars and inductively defined sets. (Jeremy)
- Lecture 2, Jan. 26: Small-step semantics. (Jeremy) Covers TAPL chapter 3.
- Lecture 3, Feb. 2: Lambda Calculus (TAPL Chapter 5). (Jonathan).
- Lecture 4, Feb. 9: Denotational Semantics of the Lambda Calculus. (Chris).
- Lecture 5, Feb. 16: ?? (??).
- Lecture 5, Feb. 23: ?? (??).
- Lecture 5, Mar. 2: ?? (??).
Lecture notes from 2008:
- Lecture 2: Inductive sets, recursive functions, proof by rule induction pdf
- Lecture 3: Small-step, Lambda Calculus, Substitution, Evaluation Contexts pdf
- Lecture 4: Big-step, DeBruijn, Locally nameless pdf
- Lecture 5: Virtual and Abstract Machines pdf
- Lecture 6: Simple Types and Type Safety pdf
- Lecture 7: More Type Safety, STLC pdf
- Lecture 8: Extensions to the STLC pdf
- Lecture 9: References, Exceptions, Normalization pdf
- Lecture 10: Subtyping pdf
- Lecture 11: More Subtyping pdf
- Lecture 12: Encoding Objects pdf
- Lecture 13: Featherweight Java pdf
- Lecture 14: Gradual Typing
- Lecture 15: Recursive Types pdf
- Lecture 16: Generics (parametric polymorphism) and System Fpdf
- Lecture 17: Existential Types pdf
- Lecture 18: Type Inference pdf
- Lecture 19: Correctness of Unification pdf