Projects
I am currently the Principal Investigator of two projects, listed below.
Constrained Higher-Order Rewriting and Program Equivalence (CHORPE – project page)). From 2021 to 2026 I will be the Principal Investigator of the NWO VIDI project CHORPE (VI.Vidi.193.075). In this project, I will work with PhD students Liye Guo and Kasper Hagens on developing methods to analyse program properties – with a particular focus on program equivalence by using term rewriting systems as an analysis language. In particular, we will consider an analysis using higher-order term rewriting systems mixed with logical constraints, to support a formalisation of traditional programs with a high level of abstraction.
Implicit Complexity through Higher Order Rewriting (ICHOR – project page)). From 2019 to 2023 I will be the Principal Investigator of a small project in NWO's TOP scheme (612.001.803/7571). In this project, I will work with PhD student Deivid do Vale on developing methods to (a) assess the inherent resource use of higher-order term rewriting systems, and (b) study higher-order computational complexity by using higher-order term rewriting systems as a tool. Both aspects will be done by imposing syntactic or semantic restrictions which bound the number of evaluation steps, and techniques such as higher-order interpretations, sharing and memoisation to bound the actual time used to reduce terms. The most import publication in this project so far are [FSCD '21] and [FSCD '23].
Past projects
In addition, listed below are the projects I have worked on in the past.
Higher Order term Rewriting for Intensional Properties of programs and circuits (HORIP – project page). From 2015 to 2017 I have worked as a postdoctoral researcher on my own Marie Curie project at the University of Copenhagen (H2020-MSCA-IF-2014, 658162). My primary focus in this topic was the characterisation of complexity classes using cons-free term rewriting systems and functional programs. The most significant papers for this project are [ESOP '17] and [LMCS '17(a)].
Constrained Rewriting and SMT: Emerging Trends in Rewriting. From 2012 to 2015 I have been employed as a postdoc on a large project at the University of Innsbruck (FWF I 963-N15) to consider term rewriting with constraints. As part of this project, I have primarily focused on (1) developing a notion of term rewriting with (arbitrary) logical constraints, and (2) using this notion towards program verification (in particular, equivalence analysis of C programs). The most significant papers for this work are [FroCoS '13] and [TOCL '17]. The tool that was developed alongside the theoretical results (Ctrl) is described on the code page. Later in the project, I have also worked on conditional rewriting, with the primary results published in [LMCS '17(b)].
Higher Order Termination. From 2007 to 2012 I have been employed as a PhD student on a project at the Free University Amsterdam (NWO-EW 612.000.629), where I considered termination of higher-order term rewriting systems. There, I developed various (interconnected) methods for proving termination of higher-order term rewriting systems, along with an automatic analysis tool that applies these results. The most significant papers for this project are [LMCS '12] and [RTA '12], and the tool (Wanda) is described on the code page. All published results and many as yet unpublished ones are explained and placed in context with each other in my PhD thesis.