CS101c

Programming Languages

Instructor: Jason Hickey (yapper.org)

Caltech Computer Science Department

Course Description

This course is covers programming language semantics, including operational, denotational, and axiomatic semantics. In addition, we will cover type systems, logic, and type theory, including type inference.

Lecture Notes

1. April 3, Introduction and administration [handouts.pdf]
2. April 8, Untyped lambda calculus [handouts.pdf]
3. April 10, Simply-typed lambda calculus [handouts.pdf]
4. April 15, Propositional Logic [handouts.pdf]
5. April 17, First and second-order Logic [handouts2.pdf]
6. April 29, Curry-Howard Isomorphism [handouts3.pdf]
7. May 1, System F [handouts1.pdf]
   1. May 6: Type inference [handouts2.pdf]
   2. May 8: Products, unions, existentials [handouts3.pdf]
8. May 12: Axiomatic szemantics [handouts.pdf]
9. May 29: Type theory [handouts.pdf]

Homeworks

1. Lambda calculus
2. System F
3. System F (part 2)
4. Imperative languages