Essentials of Programming Languages

zoom link for today is the exercises zoom link

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

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

Links