Research
Developing and maintaining software is complex and error prone. Programming languages mitigate this problem by making it easier to write software that is free of faults, through abstraction. Good programming abstractions hide irrelevant details, to facilitate higher understanding and reasoning about software, without sacrificing essential performance or programming convenience.
My research revolves around techniques and tools for building better programming abstractions, with a particular focus on abstractions-as-libraries and embedded domain-specific languages.
For an up-to-date list of my publications, see my DBLP page.
I lead, or have led, the following research projects:
Projects
Programming and Validating Software Restructurings
The project is co-funded by Philips IGT and the Dutch Research Council (NWO), and carried out using the industry-as-a-lab at Philips IGT together with researchers from TU Delft (led by me) and TU Eindhoven (led by Jan Friso Groote).
Modern software is developed by programming against libraries. As software evolves, so must the libraries. However, if we change a library interface, we must refactor code programmed against the interface. For large code bases, manually refactoring all uses of a widely used interface can be prohibitively expensive.
Automated refactoring can reduce this cost, by automatically:
Finding uses of the interface, using name binding or typing information.
Writing transformations that match and transform those occurrences to reflect the interface change.
Validating that transformations preserves behavior.
The goal of the project is to develop tooling that does this. Below is a summary of the research conducted to realize this.
Bridging the Gap Between Abstract and Concrete Syntax
A key challenge for such a tool is that it should, ideally, be usable by domain experts, who may not be intimately familiar with the particular abstract syntax tree constructors that transformation tools use behind the scenes.
To bridge this gap, we have developed an approach to defining transformations that use concrete syntax meta-patterns. Concrete syntax meta-patterns concisely pattern match on programs using the familiar concrete syntax of the programming language in question. Our approach is language-parametric in the sense that it works with an arbitrary black-box parser.
Preserving Well-Typedness of Names
Another challenge is that, as transformations move and shift code around, names may get shadowed or otherwise unreachable, depending on the scoping semantics of the language and program.
To prevent this, transformations should track which declarations each reference resolves to before the transformation. This way, we can automatically check after the transformation that each affected reference resolves to the same declaration as before. In case it does not, we can attempt to automatically add qualifiers to the name to make it resolve correctly; or report an error, in case it does not.
A paper that describes our approach to doing so is currently under submission.
Validating that Transformations Preserve Behavior
The research group at TU Eindhoven has been developing techniques based on model-checking that let us validate that restructurings preserve behavior. For example:
A new approach to model-based testing, for verifying that a system conforms to a model, such that we can efficiently verify properties of the model, such as whether the transformed program still satisfies essential behavioral properties.
Techniques for extracting models from an object-oriented interfaces, such that we can directly compare models pre- and post-transformation.
Language Support for Typed Abstractions-as-Libraries
Modern software is developed by programming against libraries. Working with such libraries corresponds to programming in a domain-specific language (DSL) inside of a general-purpose language. However, whereas modern general-purpose languages provide type checkers that can help verify the absence of errors, embedded DSLs rarely enjoy the same benefits.
In particular, most general-purpose programming languages have limited support for:
Declaring if/when a given library function can or cannot be called. For example, is a given program point allowed to have side-effects; and, if so, which?
Abstractions that have non-standard control-flow are challenging to define as library functions. For example, exceptional or resumption-based control flow, useful for search problems or asynchronous programming, generally require a different coding style, or native support (e.g., promises in JavaScript which solved the long-standing callback hell problem).
This lack of support makes software hard to debug, and causes leaky abstractions that hinder higher understanding and reasoning.
Algebraic effects and their extension to higher-order effects offers a solution to these problems.
We are working on a language that provides first-class support for higher-order effects. To this end, we have developed a core syntax and denotational semantics for a language definition language that supports both algebraic effects and handlers and higher-order effects.
Turning this syntax and model into a practical language definition language is future work. If you are interested in collaborating, I would be happy to hear from you.
Past Project
Composable and Safe-by-Construction Programming Language Definitions
This line of research was funded by a personal grant (VENI) from the Dutch Research Council (NWO) from 2019-2023.
The goals of the project were:
To develop a theoretical model of composable and safe-by-construction language definitions; and
To realize the theoretical model in a practical language definition language; i.e., a language for defining languages.
The theoretical model we adopted for the project was intrinsically typed interpreters, and we developed an approach to composing such interpreters, formalized in Agda.
The approach assumes that the interpreters being composed have the same computational effects. Unfortunately, this is not a fair assumption in general.
To compose interpreters with different effects, we need a model of composable effects. Specifically, since we are interested in defining and composing languages, we need a model of composable effects that supports effectful functions.
To this end, we developed two frameworks, latent effects and higher-order (hefty) effects, that both extend algebraic effects with support for so-called higher-order operations; i.e., effectful operations that may have computations as parameters.
We also developed a core syntax and denotational semantics for a language definition language that supports both algebraic effects and handlers, and higher-order effects.
Turning this syntax and model into a practical language definition language is future work.