Home
Welcome on my website! I am a PhD Candidate at the Programming Language Group at Delft University of Technology. Initially being supervised by Prof.Dr. Eelco Visser♱, I am now supervised by Prof.Dr. Arie van Deursen and co-supervised by Dr. Casper Bach Poulsen.
Research
My research focusses on deriving industry-quality type checkers from declarative type system specifications. In particular, I am evaluating and improving the operational aspects of Statix, while collaborating with others to use typing results of Statix to develop language-parametric transformations and editor services.
Incremental Type Checking
I am currently working on improving the performance of the concurrent Statix solver by making it automatically incremental. The goal of this work is to develop a framework for incremental type checkers that is:
- Language-independent: supports a wide range of name binding patterns.
- Type-checker paradigm independent: not bound to a particular type checker implementation strategy, such as constraint programming.
- Minimizes the effort type-checker writers need to incrementalize their type checkers.
- Sound and precise.
This work is in collaboration with Hendrik van Antwerpen, and has resulted in a publication at OOPSLA’22.
Resolution Query Compilation
A significant part of the runtime of a Statix-based type checker is used for name resolution queries (35 - 40%). Therefore, I am researching opportunities for specification compile-time optimization of queries that reduce the overhead of query resolution when analyzing an object language program.
This research has resulted in a publication at SLE’22.
Reference Retention
When moving code, references in the moved fragment can become unbound, or be captured by another definition. In this project we are exploring how scope graph can help fixing references automatically, for example by adding qualifiers. A sound solution to this problem can become the backbone of robust language-parametric transformations.
This work is in collaboration with Daniël Pelsmaeker.
Incremental Unification
Many type checkers use constraints on first-order terms to implement type inference. It is well-known how to do that efficiently using disjoint-set data structures. However, this structure does not admit incremental analysis, as it is not possibly to ‘undo’ constraints (in non-linear order). This project investigates how to support ‘undo’ operations efficiently.
Teaching
I have been involved in teaching in the following ways:
- Teaching Assistant at the 2021 edition of the Language Engineering Project course.
- Teaching Assistant at the 2021 edition of the Compiler Construction course.
- Supervisor in the 2023 edition of the Bachelor End Project: Building Type Checkers Using Scope Graphs (with Casper Bach Poulsen).
- Give Guest Lecture in 2023 edition of Language Based Software Security course (invited by Jesper Cockx). [slides].
Additionally, I have supervised two master theses:
- Boris Janssen on Bootstrapping Statix.
- Jonathan Brouwer on Expressing Dependent Types in Statix (together with Jesper Cockx).
- Alex Harsani on Embedding Statix in Agda (together with Jesper Cockx).
- Arthur de Groot on A Bottom-Up Name Resolution Algorithm for Scope Graphs (together with Jonathan Dönszelmann and Andreea Costea).
Contact
When you are interested in a teaching or research project, have another idea for collaboration, or just have a question, feel free to drop a line. My contact details are shown on the left of this page.