Publications
The following lists contain my publications to date, both formally published and informally published (workshop proceedings are listed as informally published). Links to my PhD and Master thesis are at the bottom.
In these lists, note that the downloadable version of the published paper is pre-editing. If any proofs were omitted in the paper itself, this version will also typically contain an appendix with complete proofs.
Formally published work
- 2024
-
- Rewriting
induction for higher-order constrained term rewriting systems
proceedings for LOPSTR'24 - Higher-Order
Constrained Dependency Pairs for (Universal) Computability
proceedings for MFCS'24 - Higher-Order
LCTRSs and Their Termination
proceedings for ESOP'24 - On
Basic Feasible Functionals and the Interpretation Method
proceedings for FoSSaCS'24
- Rewriting
induction for higher-order constrained term rewriting systems
- 2023
-
- Certifying
Higher-Order Polynomial Interpretations
proceedings for ITP'23 - Cost-Size
Semantics for Call-by-Value Higher-Order Rewriting
proceedings for FSCD'23
- Certifying
Higher-Order Polynomial Interpretations
- 2022
-
- Cutting a Proof
into Bite-Sized Chunks: Incrementally proving termination in higher-order term
rewriting
proceedings for FSCD'22 (Invited Paper) - Subclasses of PTIME interpreted by
programming languages
Theory of Computing Systems
- Cutting a Proof
into Bite-Sized Chunks: Incrementally proving termination in higher-order term
rewriting
- 2021
-
- Tuple
Interpretations for Higher-order Complexity
proceedings for FSCD'21
- Tuple
Interpretations for Higher-order Complexity
- 2020
-
- Cons-free
Programs and Complexity Classes between LOGSPACE and PTIME
proceedings for VPT'20 - Skylines
for Symbolic Energy Consumption Analysis
proceedings for FMICS'20 - WANDA
– a Higher-Order Termination Tool
proceedings for FSCD'20
- Cons-free
Programs and Complexity Classes between LOGSPACE and PTIME
- 2019
-
- Polymorphic
Higher-Order Termination
proceedings for FSCD'19 - A
static higher-order dependency pair framework
proceedings for ESOP'19
- Polymorphic
Higher-Order Termination
- 2017
-
- Complexity Hierarchies and
Higher-order Cons-free Term Rewriting
LMCS special issue for FSCD'16 - Verifying Procedural
Programs via Constrained Rewriting Induction
ACM TOCL 18(2) - Complexity of Conditional
Term Rewriting
(extended version of the paper Conditional Complexity in RTA '15), LMCS 13(1) - The Power of Non-Determinism in Higher-Order Implicit Complexity, proceedings for ESOP'17
- Complexity Hierarchies and
Higher-order Cons-free Term Rewriting
- 2016
-
- Complexity Hierarchies and Higher-order Cons-free Rewriting, proceedings for FSCD'16
- 2015
-
- Constrained Term Rewriting tooL, proceedings for LPAR'15 (tool paper)
- Conditional Complexity, proceedings for RTA'15
- 2014
-
- Automatic
Constrained Rewriting Induction towards Verifying Procedural Programs,
proceedings for APLAS'14
[technical report] - First-order Formative Rules, proceedings for RTA-TLCA'14
- Automatic
Constrained Rewriting Induction towards Verifying Procedural Programs,
proceedings for APLAS'14
- 2013
-
- Term Rewriting with Logical Constraints, proceedings for FroCoS'13
- 2012
-
-
Higher Order
Termination, PhD thesis at the VU University Amsterdam
Note: if you are interested in a physical copy, feel free to contact me - Polynomial Interpretations for Higher-Order Rewriting , proceedings for RTA'12
- Dynamic Dependency Pairs for Algebraic Functional Systems , LMCS special issue for RTA'11
-
Higher Order
Termination, PhD thesis at the VU University Amsterdam
- 2011
-
- Higher Order Dependency Pairs for Algebraic Functional Systems , proceedings for RTA'11
- Simplifying Algebraic Functional Systems, proceedings for CAI'11
- Harnessing First Order Termination Provers Using Higher Order Dependency Pairs, proceedings for FroCoS'11
- 2008
-
- A Higher-Order Iterative Path Ordering , proceedings for LPAR'08
Informally published work
- 2023
-
- Complexity Analysis for Call-by-Value Higher-Order Rewriting, WST'23
- Higher-order LCTRSs and their termination, HOR'23 and WST'23
- Nijn/ONijn: A New Certification Engine for Higher-Order Termination, HOR'23
- Matrix invariants for program equivalence in LCTRSs, WPTE'23
- 2022
- 2020
- 2019
- 2018
-
- Automatic termination analysis using WANDA, HOR 2018
- Improving Static Dependency Pairs for Higher-Order Rewriting, WST 2018
- 2017
- 2016
-
- Non-Deterministic Characterisations (extended abstract), WST 2016
- Higher-order Cons-free Interpreters (extended abstract), HOR 2016
- h: A Plank for Higher-order Attribute Contraction Schemes, HOR 2016
- On First-order Cons-free Term Rewriting and PTIME (extended abstract), DICE 2016
- 2014
- 2013
- 2011
-
- Dynamic Higher Order Dependency Pairs with Argument Filterings (submitted last to CADE'11; the results appear, for a different formalism, in the LMCS 2012 paper Dynamic Dependency Pairs for Algebraic Functional Systems)
- Transposing Termination Properties in Higher Order Rewriting (never submitted; the results appear in Chapter 3 of my PhD thesis)
- 2010
- 2009
Theses
- 2012
-
-
Higher Order
Termination, PhD thesis at the VU University Amsterdam
Note: if you are interested in a physical copy, feel free to contact me
-
Higher Order
Termination, PhD thesis at the VU University Amsterdam
- 2007