There are two courses:
- a seminar (4 CP) and
- a practical lab (6 CP).
Both courses are meant for advanced students interested in the lambda calculus and programming languages; functional programming design patterns (functors, monads, applicatives, lenses, …), type systems formalization and mechanization; constructive and mechanized proofs; engineering of efficient type checking, type inference algorithms; or efficient interpreters and compilers; domain-specific languages (probabilistic programming, incremental programming, choreographic programming, CRDTs, array programming, …) if they have interesting type systems.
Prerequisites: functional programming; syntax and semantics of the lambda calculus; type systems; proof techniques as in the course “Type Systems” (recommended).
Participation is limited: currently aiming for ~5 students
Application Process
Both courses target advanced students interested in programming languages and the lambda calculus. To apply, email David before 1st Oct with the following information. In your email mention the following:
Your general direction of interest, and
One concrete, recent research paper (PACMPL, ECOOP, ESOP, or associated events) that fits one of the topics of this course, described briefly in your own words:
Use DBLP to find suitable papers (PACMPL (ICFP, OOPSLA, POPL, PLDI), ECOOP, ESOP, or associated events):
Previous experiences such as course, seminars, projects that may be related to the topic and will give you a head start in understanding it.
Programming languages and what experience you have in using them (lecture, project, for fun, …). Most importantly Lean (but you can also mention other languages with interesting static type systems: Scala, Haskell, Rust, Ocaml, Rocq, TypeScript, …).
Watch out when picking papers! Some papers are more complex than others…
There is no guarantee you will work on that exact topic you propose, but your description helps us match you to supervisors or suggest other topics that we like!
You can email me even after 1st Oct, up to the end of the first week of lectures of the semester, to inquire whether further empty seats, or until I change this message and we are full.
Seminar Organisation
The seminar follows the full research workflow: topic selection, literature review, problem formulation, implementation, formalisation/mechanisation, evaluation, and scientific writing. Students present results, receive peer‑review feedback, and refine their work. The seminar language is English.
We are still deciding on the exact format, e.g.:
- one paper (<20 pages) per student in multiple milestones,
- eight 2‑page reports on different topics with iterative feedback,
- student‑led 30‑minute lectures with exercises and mutual feedback,
- or a mix of these.
Project Organisation
The project focuses on regular, git‑tracked progress implementing a research idea. Typical options include:
- re‑implementing from scratch a subset of a single complex paper,
- re‑implementing and comparing subsets of ideas from several medium‑complexity papers,
- implementing a small extension to an existing implementation from a paper,
- or similar PL‑oriented projects.
Time
Depending on whether your topic is suitable for that, it may also be possible to do the seminar and project at the same time. Keep in mind the following time-table for comparison that we are aiming for:
| what | credit | estimated workload |
|---|---|---|
| seminar | 03cp | 4 hours/week |
| lab | 06cp | 8 hours/week |
| seminar+lab | 09cp | 12 hours/week |
| (bachelor thesis) | 12cp | 16 hours/week |
| (master thesis) | 30cp | 40 hours/week |