Essentials of Programming Languages
Note
Exam Review Essentials of Programming Languages
on Monday, 2026-10-19, 10am-12pm, Pool Room 3, Werthmannstr. 4. Please bring:
- Unicard, ID document
- University account credentials
General Information
- Lecturer: Prof. Dr. Peter Thiemann
- Assistants: Marius Weidner
- Lecture: R 04 007 Videokonferenz G.-Köhler-Allee 106 and Zoom, Wednesdays 14:15-16
- Exercises: R 04 007 Videokonferenz G.-Köhler-Allee 106 and Zoom, Mondays 10-12
Lecture
| Date | Topic | Material | Recording |
|---|---|---|---|
| 2026-04-29 | Tutorial | worksheet.lagda.md | rec |
| 2026-05-06 | no lecture | ||
| 2026-05-13 | more Induction and Relations | rec | |
| 2026-05-20 | Equality | rec1, rec2 | |
| 2026-06-03 | Isomorphism, Connectives | rec | |
| 2026-06-10 | Quantifiers | rec | |
| 2026-06-17 | Lambda up to types | rec | |
| 2026-06-24 | DeBruijn up to eval | rec | |
| 2026-07-01 | Big-step semantics on DeBruijn | rec | |
| 2026-07-08 | Big-step semantics with closures | rec | |
| 2026-07-15 | Denotational Semantics | denotational_lecture.lagda | rec |
| 2026-07-22 | Interpreter, Logical Relation | Interpreter-2026.lagda | rec |
| 2026-08-12 | Q&A | will not be recorded |
Tutorial
| Date | Chapter | Material | Recording |
|---|---|---|---|
| 2026-04-27 | Getting Started | intro.agda | rec |
| 2026-05-04 | Naturals | naturals.agda | rec |
| 2026-05-11 | Induction | induction.agda | rec |
| 2026-05-18 | Relations | relations.agda | rec |
| 2026-06-01 | Equality, Isomorphism | equality.agda, extensionality.agda, paradoxes.agda | rec |
| 2026-06-08 | Isomorphism, Connectives, Negation | isomorphism.agda, connectives.agda, negation.lagda | rec |
| 2026-06-15 | Negation, Quantifiers, Decidable | negation.agda, quantifiers.agda, decidability.lagda | rec |
| 2026-06-22 | Decidable, Lambda | decidable.agda, lambda.agda | rec |
| 2026-06-29 | Properties, DeBruijn | lambda.agda, intrinsic-extrinsic.agda | rec |
| 2026-07-06 | Properties, DeBruijn | intrinsic-extrinsic.agda | rec |
| 2026-07-13 | DeBruijn | intrinsic-extrinsic.agda | rec |
| 2026-07-20 | DeBruijn | denotational.agda | rec |
Exam
| Date | Time | Place | Mode |
|---|---|---|---|
| tba | tba | tba | computer ∣ closed book |