Syllabus

This course is an introduction to the mathematical techniques for defining programming languages, analyzing their behavior, and proving properties about them.

Lecture: Tuesdays and Thursdays, 9:30-10:45am, in LH 035.

Instructor: Jeremy Siek (jsiek), Office hours: Tue 4-5pm, Thu 1:30-2:30pm, Office: LH 230D

Associate Instructor: Wren Romano (wrengr), Office hours: weekdays 1-4pm but email 24 hours ahead of time, Office: LH 330I

Textbooks:

  • TAPL: Types and Programming Languages by Benjamin C. Pierce
  • PLT: Semantics Engineering with PLT Redex by Matthias Felleisen, Robert Bruce Findler and Matthew Flatt

Resources:

Schedule:

  1. Logic, Proof, and Functional Programming (LogicRef.thy, Chapter1.thy)
    • Isabelle file from lecture
    • Reading: Course Notes Ch. 1, TAPL Ch. 1 and 2, Optional Reading: Isabelle Tutorial Ch. 1 and 2
    • Exercises: 1 through 5 from the Course Notes, due in class 1/20
  2. Semantics of a Primitive Language (Chapter2.thy)
  3. Variables Chapter3.thy
    • Isabelle file from lecture
    • Reading: Course Notes Ch. 3, TAPL Ch. 5 and 8
    • Exercises: 8 and 9 from the Course Notes, due in class 2/17
  4. Lambda Calculus Chapter4.thy
    • Reading: Course Notes Ch. 4, TAPL Ch. 6, 9, and 12
    • Exercises: 10 from the Course Notes, due in class 2/24
    • Wren's lecture notes and Coq proofs are here
  5. Mutable State Chapter5.thy
    • Reading: Course Notes Ch. 5, TAPL Ch. 13
  6. Exceptions and Continuations
    • Reading: Course Notes Ch. 6, TAPL Ch. 14, PLT Ch. 5 Sec. 1, PLT Ch. 8
  7. Abstract Machines
    • Reading: Course Notes Ch. 7, PLT Ch. 6
  8. Generics
  9. Recursive Types and Datatype Encodings
    • Reading: TAPL Ch. 20 and Ch. 21
  10. Concurrency and CCS
  11. Behavioral Equivalences and Coinduction
    • Reading: RSMSV Ch. 3 (section 1 to 4, ok to skip the proofs) and Ch. 4
  12. Mobility and the Pi-calculus
  13. The Abella Theorem Prover
  14. Final Exam solution


© Jeremy Siek 2015