## 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.