Projecten
Ik ben op dit moment actief als Principal Investigator van twee projecten, hieronder beschreven.
Constrained Higher-Order Rewriting and Program Equivalence (CHORPE – project pagina)). Van 2021 tot 2026 zal ik de Principal Investigator zijn van het NWO VIDI project CHORPE (VI.Vidi.193.075). In dit project zal ik samenwerken met promovendi Liye Guo en Kasper Hagens aan het ontwikkelen van methodes om programma-eigenschappen te ontwikkelen – in het bijzonder geconcentreerd op programma equivalentie. We doen dit door gebruikt te maken van termherschrijven als analysetaal. In het bijzonder zullen we een analyse ontwikkelen gebaseerd op hogere orde termherschrijven, gecombineerd met logische beperkingen. Het vermoeden is dat dit het mogelijk maakt om traditionele programma's naar een analysetaal te vertalen met behoud van een hoog abstractieniveau.
Implicit Complexity through Higher Order Rewriting (ICHOR – project pagina)). Van 2019 tot 2023 zal ik de Principal Investigator zijn van een project in het NWO TOP schema (612.001.803/7571). In dit project zal ik samen met promovendus Deivid do Vale werken aan het ontwikkelen van methodes om (a) te analyseren hoeveel resources nodig zijn voor het reduceren van bepaalde types hogere orde termherschrijfsystemen (in het bijzonder tijd en ruimte), en (b) complexiteitsklassen te karakteriseren met gebruik van hogere orde termherschrijfsystemen. Hiervoor zullen we zowel syntactische en semantische beperkingen opleggen die het aantal evaluatiestappen dat gedaan kan worden op een term begrenzen, en technieken zoals hogere orde interpretaties, het delen van geheugen en opslaan van tussenresultaten om hier ook daadwerkelijk een begrenzing uit te krijgen. De belangrijkste projectresultaten tot nog toe zijn beschreven in [FSCD '21] en [FSCD '23].
Afgeronde projects
Projecten waar ik in het verleden aan heb gewerkt staan hieronder beschreven.
Higher Order term Rewriting for Intensional Properties of programs and circuits (HORIP). Van 2015 tot 2017 heb ik gewerkt aan mijn eigen Marie Curie project aan de Universiteit van Kopenhagen (H2020-MSCA-IF-2014, 658162). Dit ging voornamelijk over het karakteriseren van complexiteitsklassen met "cons-free" termherschrijfsystemen en functionele programma's. De belangrijkste papers voor dit project zijn [ESOP '17] en [LMCS '17(a)]. Een overzicht over de resultaten van HORIP is los bschikbaar.
Constrained Rewriting and SMT: Emerging Trends in Rewriting. Van 2012 to 2015 ben ik als postdoc betrokken geweest bij een groot project bij de Universiteit van Innsbruck (FWF I 963-N15) over termherschrijven met beperkingen. Als deel van dit project heb ik me voornamelijk geconcentreerd op (1) het ontwikkelen van een uitbreiding van standaard termherschrijfsystemen met (wikkekeurige) logische beperkingen, en (2) het gebruik van deze systemen voor programmaverificatie (en in het bijzonder: equivalentie-analyse van programma's in C). De belangrijkste papers voor dit deel van het project zijn [FroCoS '13] en [TOCL '17]. Het tool dat we hebben ontwikkeld naast de theoretische resultaten staat beschreven op de code pagina. Later in het project heb ik ook gewerkt aan herschrijven met condities; hiervan zijn de voornaamste resultaten te vinden in [LMCS '17(b)].
Higher Order Termination. Van 2007 to 2012 heb ik als promovendus gewerkt aan een project aan de Vrije Universiteit Amsterdam (NWO-EW 612.000.629) dat ging over terminatie van hogere orde termherschrijfsystemen. Daar heb ik diverse (sterk met elkaar samenhangende) methodes ontwikkeld om terminatie te bewijzen van hogere orde termherschrijfsystemen. Hiernaast heb ik een tool geïmplementeerd dat deze resultaten automatisch kan toepassen. De voornaamste papers voor dit project zijn [LMCS '12] en [RTA '12], en het tool (Wanda) staat bescreven op de code pagina. Alle gepubliceerde en ook een groot aantal nog niet gepubliceerde resultaten zijn volledig uitgewerkt en in onderlinge context beschreven in mijn proefschrift.