This seminar is 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.
This description is still under construction. The registration deadline may be before or in the first week of the semester. For a complete description, please check back on 5th October.
There will be two courses:
- a seminar (4 CP) and
- a practical lab (6 CP).
Prerequisites: functional programming; syntax and semantics of the lambda calculus; type systems; proof techniques as in the course “Type Systems” (recommended).
Participation is limited: likely ~5 students in the seminar and in the lab.
Topics and Registration
Both courses target advanced students interested in programming languages and the lambda calculus. To register, email David before the start of the semester with:
Your general direction of interest, and
One recent research paper (PACMPL, ECOOP, ESOP, or associated events) that fits one of the following areas, described briefly in your own words:
Use DBLP to find suitable papers (PACMPL (ICFP, OOPSLA, POPL, PLDI), ECOOP, ESOP, or associated events):
Watch out! Some papers are more complex than others…
There is no guarantee you will work on that exact topic, but your description helps us match you to supervisors or suggest related topics.
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,
- 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.