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:**

- Course Notes
- Course Email Group (on Piazza)
- Isabelle Proof Assistant
- Isabelle Tutorial: A Proof Assistant for Higher-Order Logic by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel
- Programming and Proving in Isabelle/HOL by Tobias Nipkow
- PL Semantics in Isabelle: Concrete Semantics by Tobias Nipkow and Gerwin Klein
- Isabelle/Isar Reference Manual by Makarius Wenzel
- Jeremy’s Blog
- wrengr-util — a collection of tactics, lemmas, and definitions for Coq. In particular, it includes definitions for working with closures of binary relations.
- coq-tutorial — some notes from my Coq tutorial sessions.

**Schedule:**

- 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

- Semantics of a Primitive Language (Chapter2.thy)
- Isabelle file from lecture
- Reading: Course Notes Ch. 2, TAPL Ch. 3
- Exercises: 6 and 7 from the Course Notes, due in class 2/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

- 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

- Mutable State Chapter5.thy
- Reading: Course Notes Ch. 5, TAPL Ch. 13

- Exceptions and Continuations
- Reading: Course Notes Ch. 6, TAPL Ch. 14, PLT Ch. 5 Sec. 1, PLT Ch. 8

- Abstract Machines
- Reading: Course Notes Ch. 7, PLT Ch. 6

- Generics
- Reading: Notes on parametricity, TAPL Ch. 23 and Ch. 24

- Recursive Types and Datatype Encodings
- Reading: TAPL Ch. 20 and Ch. 21

- Concurrency and CCS
- Reading: Ch. 1 and 2 of Reactive Systems: Modeling, Specification, and Verification (RSMSV)

- Behavioral Equivalences and Coinduction
- Reading: RSMSV Ch. 3 (section 1 to 4, ok to skip the proofs) and Ch. 4

- Mobility and the Pi-calculus
- Reading: An Introduction to the pi-Calculus.

- The Abella Theorem Prover
- Final Exam solution