Implicit Complexity through Higher Order Rewriting (ICHOR)
From September 2019 to September 2023 I will lead the NWO TOP
project Implicit Complexity through Higher Order Rewriting, grant
number 612.001.803/7571. This page lists the work performed as part of
this project.
Project goals
The goal of ICHOR is to study computational complexity of and using
higher-order term rewriting systems. Our particular focus is to develop methods
that involve algebra interpretations.
Publications
To date, the project has resulted in six publications in formal conference/workshop
proceedings, and seven informal papers.
Use the green download buttons to obtain the author copies.
Publications in journals
- Subclasses of PTIME interpreted by programming languages,
by Siddharth Bhaskar, Cynthia Kop and Jakob Grue Simonsen, Theory of Computing Systems 2022
Publications in formal conference/workshop proceedings
- Certifying Higher-Order Polynomial Interpretations,
by Niels van der Weide, Deivid Vale and Cynthia Kop, proceedings for ITP 2023
- Cost-Size Semantics for Call-By-Value Higher-Order Rewriting,
by Cynthia Kop and Deivid Vale, proceedings for FSCD 2023
-
-
Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting,
by Cynthia Kop, proceedings for FSCD 2022
-
-
Tuple Interpretations for Higher-Order Complexity,
by Cynthia Kop and Deivid Vale, prceedings for FSCD 2021
-
-
Nominal Equational Problems,
by Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho and Deivid Vale, proceedings for FoSSaCS 2021
-
-
Cons-free Programs and Complexity Classes between LOGSPACE and PTIME by Neil Jones, Siddharth Bhaskar, Cynthia Kop and Jakob Grue Simonsen, proceedings for VPT 2020
Publications in informal workshop proceedings

- Complexity Analysis for Call-by-Value Higher-Order Rewriting,
by Cynthia Kop and Deivid Vale, proceedings for WST 2023

- Nijn/ONijn: A New Certification Engine for Higher-Order Termination,
by Cynthia Kop, Deivid Vale and Niels van der Weide, proceedings for HOR 2023

- Analyzing Innermost Runtime Complexity Through Tuple Interpretations,
by Liye Guo and Deivid Vale, proceedings for LSFA 2022
- Tuple Interpretations and Applications to Higher-Order Runtime Complexity
by Cynthia Kop and Deivid Vale, proceedings for WST 2022
- Nominal Disunification via Fixed-Point Constraints,
by Leonardo M. Batista, Maribel Fernández, Daniele Nantes-Sobrinho and Deivid Vale,
proceedings for UNIF 2021
-
-
Formalizing higher-order termination in COQ
by Deivid Vale and Niels van der Weide, proceedings for WST 2021
-
-
Tuple Interpretations for Higher-Order Complexity (extended abstract)
by Cynthia Kop and Deivid Vale, proceedings for LCC 2020
Submitted to journals and conferences
- Complexity Analysis through Tuple Interpretations,
by Liye Guo and Deivid Vale; submitted to Mathematical Structures in Computer Science (MSCS) for the special issue of LSFA 2022.
- On Basic Feasible Functionals and the Interpretation Method,
by Patrick Baillot, Ugo dal Lago, Cynthia Kop and Deivid Vale;
submitted to FoSSaCS 2024.
Project members
 |
 |
Cynthia Kop |
Deivid Vale |