Teaching Material
Here, you can find the material used in the lectures and in the lab sessions. To navigate through the slides, you can use the left and right arrows to enter slide mode; press ESC to go back to normal.
Week 1 (01/03)
- Lecture 1 slides (Introduction to the course)
- Recommended reading: The Programming Languages Enthusiast blogpost series on Authenticated Data Structures (Generically)
(If you want to read the technical paper on the PL-based solution, there's a preprint available.) - Lecture 2 slides (Introduction to Coq: Basic Functional Programming)
Files: L02_live.v
Week 2 (08/03)
- Lecture 3 slides (Working with Structured Data and Polymorphism)
Files: L03_Live.v - Lab Session 1: Exercises
(Solutions) - Lecture 4 slides (Polymorphism and Higher-Order Functions)
Files: L04_Live.v
Week 3 (15/03)
- Lecture 5 slides (Higher-Order Functions and Proving in Coq)
Files: L05_live.v - Lab Session 2: Exercises
(Solutions) - Lecture 6 slides (Proving in Coq)
Files: L06_live.v
Week 4 (22/03)
- Lecture 7 slides (Programming Language Syntax)
- Lab Session 3: Exercises
(Solutions) - Lecture 8 slides (ASTs, Variables, Bindings, Scopes)
Files: TacticsLP.v, L08_live.v
Week 5 (05/04)
- Lecture 9 slides (Semantics via interpreters: arithmetic and a stack machine)
Files: Maps.v (from the SF book), L09_live.v - Lab Session 4: Exercises
(Solutions) - Lecture 10 slides (Semantics via interpreters; towards imperative programming languages)
Files: L10_pre.v
Week 6 (12/04)
- Lecture 11 slides (Evaluation as a Relation)
Whiteboard notes
Link to Software Foundations (Volume 1): https://softwarefoundations.cis.upenn.edu/lf-current/index.html
File with Software Foundations (Volume 1): lf.tgz - Lab Session 5: Exercises
(Selected Solutions) - Lecture 12 slides (Evaluation as a Relation, continued)
Week 7 (19/04)
- Lecture 13 slides (Evaliation as a Relation: Hands-on-Approach)
Link to Software Foundations (Volume 1): https://softwarefoundations.cis.upenn.edu/lf-current/index.html
File with Software Foundations (Volume 1): lf.tgz - Lab Session 6: groups should work on the first project
- Lecture 14 slides (Hoare Logic)
Link to Software Foundations (Volume 2): https://softwarefoundations.cis.upenn.edu/plf-current/index.html
File with Software Foundations (Volume 2): plf.tgz
Week 8 (26/04)
- Lecture 15 slides (Hoare Logic, continued)
- Lab Session 7: groups should work on the first project
- Lecture 16: Revision/Consolidation for Test 1 + Hoare Logic
Week 9 (03/05)
- Lecture 17: Selected exercises on Hoare Logic + Decorated Programs + "Hoare Logic as a Logic"
Links to chapters: Hoare.v , Hoare2.v, and HoareAsLogic.v - Lab Session 8: List of Activities
- Lecture 18: Small-step semantics
Support file: Lecture18.v (load it from the same folder as Volume 2 --- PLF)
File with all solutions: Lecture18_solutions.v
Week 10 (10/05)
- Lecture 19: Introduction to Types
File used in the lecture: Lecture19.v - Lab Session 9: Exercises
(Solutions) - Lecture 20: Lambda Calculus
Week 11 (17/05)
- Lecture 21: The Simply Typed Lambda Calculus
File used in the lecture: Lecture21.v (load it from the same folder as Volume 2 --- PLF)
File with solutions: Lecture21_solutions.v - Lab Session 10: Exercises
(Solutions)
Week 12 (24/05)
- Lecture 22: Typechecking and Subtyping
File used in the lecture: Lecture22.v (load it from the same folder as Volume 2 --- PLF) - Lab Session 11: groups should work on the second project
- Lecture 23: Records and Subtyping (cont.)
File used in the lecture: Lecture23.v (load it from the same folder as Volume 2 --- PLF)
Week 13 (31/05)
- Lecture 24: Guest Lecture, Ralf Jung (MPI-SWS & MIT), Tutorial on Iris
- Lab Session 12: groups should work on the second project
- Lecture 25: Records and Subtyping (consolidation / exercises)
We used the file discussed previously: Lecture23.v (load it from the same folder as Volume 2 --- PLF)
Complete file: Lecture23_solution.v