Master of Programming Languages

For students participating in the TU Delft Computer Science and Embedded Systems master’s programs we always have openings for master’s thesis projects.

All master’s thesis projects are aligned with our research. They often are connected to one of our ongoing research projects, but we also frequently use master’s projects to explore new research directions.

Note that research is rarely finished and that projects often generate new research questions. If you are interested in the topic of one of the ongoing or closed projects below, do contact the supervisors to find out if there is more to do in that area.

Project Location

Projects can be conducted at:

  • TU Delft in our own research labs, in close collaboration with our postdocs and PhD students
  • Industry (as part of an internship), usually with companies (in The Netherlands or abroad) with which we have an ongoing research collaboration (e.g. Oracle, Canon Production Printing [formerly Océ], ING, …)
  • Other (international) universities – we have a rich network of academic friends around the world.
Supervisors

You can make an appointment with one of the PL faculty members to see what projects are currently open, or you can propose your own project, provided there is a clear connection with the research we conduct at our labs.

Composing your Study Program

If you plan to conduct your master’s project at PL, you will need to include at least two of the CS master’s courses PL teaches in your IEP (Individual Exam Program). We strongly recommend you to follow our compiler construction and programming languages seminar courses. Besides our own programming languages related courses, when choosing the electives in your program you can consider including courses in such areas as software engineering, machine learning, data science, distributed systems, and security.

Optionally, you can start your research with a 7-8 week literature survey (IN4306, 10EC). This assignment is concluded with a report containing an overview of the state-of-the-art in a particular branch of research.

Proposing your Own Project

Under certain conditions it can also be possible to propose your own project. In those cases it is important to

  • Study a number of previous master’s theses
  • Identify an ongoing research project to which your proposal is connected.
  • Study a number of currently open master’s project ideas and identify the ones that are closest to your idea.

In particular you need to carefully think about the research component of your proposal, and have a clear idea on why your proposal is novel — it should advance the state-of-the-art in programming languages. If you wish to pursue this route it is advisable to select and contact a possible supervisor as early as possible.

Thesis Template

As a template for your master thesis, it is recommended that you fork the PL Master Thesis LaTeX Template repository, and manage your references at researchr.org.

Open Projects

Formalizing "Weakest preconditions in fibrations"

Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: November 04, 2024

Formalizing and comparing categorical structures for type dependency

Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: November 04, 2024

Extending the Agda Core project

Supervisor(s): Jesper Cockx
Posted: August 01, 2024

A type system for run-time identity functions

Supervisor(s): Jesper Cockx
Posted: July 19, 2024

Incremental and parallel checking of dependently typed programs

Supervisor(s): Jesper Cockx
Posted: April 15, 2024

Proving Binary Translation between Architectures

Supervisor(s): Dennis Sprokholt, Soham Chakraborty
Posted: April 12, 2023

Analysis and Testing for Weak Memory Concurrency

Supervisor(s): Soham Chakraborty
Posted: April 12, 2023

Implementation and verification of an SMT solver

Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: March 14, 2023

Computer formalization of Voevodsky's theory of type theories

Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: June 05, 2022

Universe Management in UniMath

Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: April 25, 2022

Porting Concurrent Applications between Architectures.

Supervisor(s): Soham Chakraborty
Posted: September 14, 2021

Static Binary Translation of Concurrency

Supervisor(s): Soham Chakraborty
Posted: June 05, 2021

Ongoing Projects

Domain-specific Abstractions for Algorithmic Graph Processing

Student: Jochem Broekhoff
Supervisor(s): Jesper Cockx

Combining dependent types with dynamic checks and monitoring

Student: Jakob Naucke
Supervisor(s): Jesper Cockx, Bohdan Liesnikov

An evaluation of algorithms for conversion checking

Student: Ksawery Radziwiłowicz
Supervisor(s): Jesper Cockx

Formalizing "Classical lambda calculus in modern dress"

Student: Arnoud van der Leer
Supervisor(s): Benedikt Ahrens, Kobe Wullaert

t.b.a.

Student: Ruben van Baarle
Supervisor(s): Casper Bach Poulsen

Previous Projects

Embedding Statix in Agda

Student: Alex Harsani
Supervisor(s): Aron Zwaan, Casper Bach Poulsen, Jesper Cockx

Program Synthesis for Dependently Typed Programs

Student: Luka Janjić
Supervisor(s): Jesper Cockx, Sebastijan Dumancic

Model checking the XMM memory model

Student: Matteo Meluzzi
Supervisor(s): Soham Chakraborty
Defended: July 03, 2024

Can The Language Server Protocol Handle Dependent Types?

Student: Willem Stuijt Giacaman
Supervisor(s): Jesper Cockx, Daniël Pelsmaker
Defended: June 26, 2024

Replication and formalization of (Co)Church encoded shortcut fusion

Student: Eben Rogers
Supervisor(s): Casper Bach Poulsen, Jaro Reinders
Defended: June 24, 2024

Verifying weak memory concurrent data structure implementations

Student: Casper Henkes
Supervisor(s): Soham Chakraborty

Modal μ-Calculus for Free

Student: Ivan Todorov
Supervisor(s): Casper Bach Poulsen
Defended: June 28, 2024

Modeling and Analysis of System-on-Chip Address Maps

Student: Niels Mook
Supervisor(s): Soham Chakraborty

Dependently Typed Languages in Statix

Student: Jonathan Brouwer
Supervisor(s): Jesper Cockx, Aron Zwaan
Defended: April 26, 2023

Bootstrapping the statix meta-language

Student: Boris Janssen
Supervisor(s): Aron Zwaan, Benedikt Ahrens, Matthijs Spaan, Eelco Visser†
Defended: April 17, 2023

Efficient Execution of User-Provided Graph Algorithms in a Graph Database

Student: Daan de Graaf
Supervisor(s): Soham Chakraborty
Defended: August 30, 2023

Modernizing the WebDSL front-end: A case study in SDF3 and Statix

Student: Max de Krieger
Supervisor(s): Danny Groenewegen, Jesper Cockx, Arie van Deursen, Eelco Visser†
Defended: December 21, 2022

Proving functional correctness of monadic programs using separation logic

Student: Liam Clark
Supervisor(s): Robbert Krebbers, Jesper Cockx, Andy Zaidman
Defended: December 02, 2022

Fencing off unwanted behavior: Improving and evaluating the Fency static analysis tool

Student: Pieter van den Ham
Supervisor(s): Dennis Sprokholt, Soham Chakraborty, Koen Langendoen
Defended: December 02, 2022

Dependent Type-Checking Modulo Associativity and Commutativity

Student: Lucas Holten
Supervisor(s): Jesper Cockx, Lucas Escot
Defended: September 12, 2023

A Domain Specific Language for Modeling Intelligent Print Systems

Student: Bram van Walraven
Supervisor(s): Jasper Denkers, Benedikt Ahrens, Eelco Visser†
Location: Canon Production Printing (Venlo), TU Delft
Defended: November 09, 2022

Elaine: Elaborations of Higher-Order Effects as First-Class Language Feature

Student: Terts Diepraam
Supervisor(s): Casper Bach Poulsen, Cas van der Rest
Defended: September 28, 2023

Towards Automatic Test Suite Generation for Functional Programming Assignments using Budgeted Compositional Symbolic Execution

Student: Wesley Baartman
Supervisor(s): Casper Bach Poulsen, Koen Langendoen
Defended: October 26, 2022

A universal format for code base metadata

Student: Jonathan Dönszelmann
Supervisor(s): Daniël Pelsmaeker, Jesper Cockx

Bringing Formal Verification into Widespread Programming Language Ecosystems

Student: Sara Juhosova
Supervisor(s): Lucas Escot, Jesper Cockx
Defended: June 29, 2023

A generic translation from case trees to eliminators

Student: Kayleigh Lieverse
Supervisor(s): Lucas Escot, Jesper Cockx
Defended: June 20, 2024

Improving Agda's module system

Student: Ivar de Bruin
Supervisor(s): Bohdan Liesnikov, Jesper Cockx
Defended: July 05, 2023

Tactics in Agda using reflection

Student: Paul van der Stel
Supervisor(s): Bohdan Liesnikov, Jesper Cockx, Andy Zaidman
Defended: September 21, 2022

Probabilistic Testing for Weak Memory Concurrency

Student: Mingyu Gao
Supervisor(s): Soham Chakraborty
Defended: September 05, 2022

Dynamix: A Domain-Specific Language for Dynamic Semantics

Student: Thijs Molendijk
Supervisor(s): Casper Bach Poulsen, Andrew Tolmach (Portland State University), Eelco Visser
Defended: August 30, 2022

Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda

Student: Olav de Haas
Supervisor(s): Arjen Rouvoet, Jesper Cockx, Eelco Visser
Defended: July 11, 2022

Extending the Domain Specific Language for the Pipelines for Interactive Environments build system

Student: Ivo Wilms
Supervisor(s): Gabriël Konat, Casper Bach Poulsen, Eelco Visser
Defended: July 01, 2022

Dataflow Analysis in a Language Workbench

Student: Matthijs Bijman
Supervisor(s): Jeff Smits, Soham Chakraborty, Eelco Visser
Defended: June 29, 2022

Function Inlining as a Language Parametric Refactoring

Student: Loek van der Gugten
Supervisor(s): Luka Miljak, Casper Bach Poulsen, Eelco Visser
Defended: June 22, 2022

Describing Inter Parameter Constraints in Web APIs Using Dependent Types

Student: Gerben Oolbekkink
Supervisor(s): Casper Bach Poulsen, Eelco Visser
Defended: May 17, 2022

Optimising First-Class Pattern Match Compilation

Student: Toine Hartman
Supervisor(s): Jeff Smits, Eelco Visser
Defended: February 23, 2022

Deriving Effect Handler Semantics

Student: Chris Lemaire
Supervisor(s): Jaro Reinders, Casper Bach Poulsen
Defended: March 29, 2023

Incremental Scannerless Generalized LR Parsing

Student: Maarten Sijm
Supervisor(s): Jasper Denkers, Eelco Visser
Defended: July 14, 2021

Renaming for Everyone - Language-Parametric Renaming in Spoofax

Student: Phil Misteli
Supervisor(s): Daniël Pelsmaeker, Casper Bach Poulsen, Eelco Visser
Defended: May 25, 2021

Compiling with Command Trees

Student: Bernard Bot
Supervisor(s): Casper Bach Poulsen, Eelco Visser
Defended: May 19, 2021

Framing Programming Languages: Designing and Using a Frame-Based Virtual Machine

Student: Bram Crielaard
Supervisor(s): Casper Bach Poulsen, Eelco Visser
Defended: April 21, 2021

Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq

Student: Jens de Waard
Supervisor(s): Robbert Krebbers, Eelco Visser
Defended: February 03, 2021

Composable Type System Specification using Heterogeneous Scope Graphs

Student: Aron Zwaan
Supervisor(s): Eelco Visser
Defended: January 27, 2021

Expressing Intent

Student: Jeroen Kloppenburg
Supervisor(s): Soham Chakraborty, Koen Langendoen
Defended: July 11, 2023

Comparing Static Semantics Specifications for the IceDust DSL: A Case Study of Statix

Student: Jesse Tilro
Supervisor(s): Danny Groenewegen, Eelco Visser, Benedikt Ahrens
Defended: September 13, 2023

Dynamix on the Frame VM: Declarative dynamic semantics on a VM using scopes as frames

Student: Chiel Bruin
Supervisor(s): Casper Bach Poulsen, Eelco Visser
Defended: April 29, 2020

Redesigning the Spoofax Testing Language

Student: Volker Lanting
Supervisor(s): Gabriël Konat, Eelco Visser
Defended: January 29, 2020

Incrementalizing Statix: A Modular and Incremental Approach for Type Checking and Name Binding using Scope Graphs

Student: Taico Aerts
Supervisor(s): Hendrik van Antwerpen, Eelco Visser
Defended: September 26, 2019

A type system for dynamic instances

Student: Albert ten Napel
Supervisor(s): Robbert Krebbers, Eelco Visser
Defended: September 05, 2019

Task Observability in change driven incremental build systems with dynamic dependencies

Student: Roelof Sol
Supervisor(s): Gabriël Konat, Eelco Visser
Defended: August 29, 2019

SCL-T - Template programming for Siemens SCL

Student: Jeffrey Goderie
Supervisor(s): Casper Bach Poulsen, Eelco Visser
Defended: August 29, 2019

Dependent Types for Invariants in Session Types

Student: Wiebe van Geest
Supervisor(s): Casper Bach Poulsen, Eelco Visser
Defended: December 14, 2018

Testing Code Generators against Definitional Interpreters

Student: Giannis Papadopoulos
Supervisor(s): Sebastian Erdweg, Eelco Visser
Defended: December 05, 2018

Incremental Type Checking in IncA

Student: Sander Bosma
Supervisor(s): Sebastian Erdweg, Eelco Visser
Defended: November 02, 2018

Abstract Interpretation of Program Transformations using Regular Tree Grammars

Student: Jente Hidskes
Supervisor(s): Sebastian Erdweg, Eelco Visser
Defended: November 02, 2018

Towards Language Parametric Web-Based Development Environments

Student: Olaf Maas
Supervisor(s): Eelco Visser
Defended: July 13, 2018

Portable Editor Services

Student: Daniël Pelsmaeker
Supervisor(s): Gabriël Konat, Eelco Visser
Defended: May 03, 2018

The Design and Implementation of a Domain-Specific Language for the Description of Medical Devices

Student: Tim Rensen
Supervisor(s): Eelco Visser
Defended: April 18, 2018

Random Term Generation for Compiler Testing in Spoofax

Student: Martijn Dwars
Supervisor(s): Hendrik van Antwerpen, Eelco Visser
Defended: March 12, 2018

AlanLight

Student: Gerben Kunst
Supervisor(s): Daco Harkes, Eelco Visser
Defended: January 30, 2018

A Modular SGLR Parsing Architecture for Systematic Performance Optimization

Student: Jasper Denkers
Supervisor(s): Eduardo de Souza Amorim, Eelco Visser
Defended: January 24, 2018

TODO: add links to (more) previous theses and student papers