Programming Languages Calendar

The PL group organizes a weekly lunch seminar on Wednesdays from 12:00 to 13:00 in which one of the group members or a visitor gives a talk. Occasionally we have `progress' lunches in which everyone gives an update about what they are doing.

To subscribe to our calendar, use the following link: https://pl.ewi.tudelft.nl/pl-events.ics

To edit the events, refer to the event instructions.

Upcoming Events

Seminar
Deep Instantiation Meets Dependent Typing: The Potential of Coding Potency in Potent Type Systems
Ralf Lämmel

Wednesday, 30 September 2026 @ 11:00 - 12:00
28 - Hilbert

Multi-level modelling (MLM) extends conventional modelling by classification hierarchies that span more than two levels, concepts such as deep instantiation and level-crossing relationships. While several formal foundations for MLM have been the potential of contemporary dependent type systems a semantic basis has received comparatively little attention. This therefore explores the idea of encoding multi-level models in type systems of languages such as Scala, Lean, and Haskell, feature dependent types, type families, and other advanced constructs. Although we limit ourselves to a simple setup of instantiation here, our findings suggest that this idea may indeed be valuable for exploring the design space of MLM languages.
Seminar
Mauricio Verano Merino

Wednesday, 14 October 2026 @ 13:45 - 14:45
28 - Social Data Lab

PhD Defense
Language-Parametric Editor Services from Language Specifications
Daniel A.A. Pelsmaeker

Wednesday, 11 November 2026 @ 17:30 - 19:00
Aula - Senaatzaal

Available Slots

The current slots are currently available for seminar. Please reach out if you would like to give a talk!

  • Wednesday, 07 October 2026 @ 12:00 - 13:00
  • Wednesday, 21 October 2026 @ 12:00 - 13:00
  • Wednesday, 28 October 2026 @ 12:00 - 13:00
  • Wednesday, 04 November 2026 @ 12:00 - 13:00
  • Wednesday, 11 November 2026 @ 12:00 - 13:00
  • Wednesday, 18 November 2026 @ 12:00 - 13:00
  • Wednesday, 25 November 2026 @ 12:00 - 13:00
  • Wednesday, 09 December 2026 @ 12:00 - 13:00
  • Wednesday, 16 December 2026 @ 12:00 - 13:00
  • Wednesday, 23 December 2026 @ 12:00 - 13:00

If you are a member of the group, refer to the event instructions on information about how to claim a slot.

Past Events

MSc Defense
Georgi Nihrizov

Monday, 21 September 2026 @ 16:00 - 17:30
28 - 5.C960 Ritchie

Seminar
Type-Based Library Search for Theorem Provers
Satoshi Takimoto

Wednesday, 16 September 2026 @ 12:00 - 13:00
28 - Hilbert

In this talk, I present my ongoing PhD research on type-based library search for theorem provers. The talk consists of two parts. In the first half, I discuss type-based candidate matching, focusing on the behavior that such a matching procedure should support. The second half is about candidate pre-filtering, and we briefly see a natural connection to abstract interpretation. I focus on developing a "semantic specification" of type-based library search that will serve as a guide for the development and evaluation of actual algorithms. Algorithmic details will be left for another opportunity.
Seminar
A compiler for quantum and classical computation
Sacha Bernheim

Wednesday, 09 September 2026 @ 12:00 - 13:00
28 - Hilbert

For our next PL seminar, we’ll have Sacha Bernheim from QuTech giving a talk on his experience designing a compiler for quantum internet programs. While this might sound somewhat far from our area, a discussion with Sacha and his PhD supervisor, Stephanie Wehner, made it clear that there is actually quite a bit of potential overlap with some of our works. I invited Sacha to give this talk both in the hope of finding some research synergies between the PL and QuTech groups, and to satisfy our/my curiosity about what folks at QuTech are working on.
Seminar
NbE for LNL via Adjoint Meta-Modalities
James Wood

Wednesday, 02 September 2026 @ 12:00 - 13:00
28 - Hilbert

There will be pizza served at this event!

In this talk, I recap normalisation by evaluation (NbE) on the Simply Typed lambda-Calculus, develop the same for Linear Logic, and then combine those two to get an NbE procedure for Linear/Non-Linear Logic (LNL). I use intrinsically well typed representations together with meta-connectives based on Rouvoet et al's Proof Relevant Separation Logic to get a clean and well factored mechanisation. In LNL, type formers F and G get metatheory-level counterparts to relate linear and Cartesian judgements, which I call meta-modalities.
MSc Defense
Gijs van der Heide

Tuesday, 01 September 2026 @ 17:30 - 19:00
28 - 1.W510 Banach