Implicit Complexity through Higher Order Rewriting (ICHOR)

From September 2019 to September 2023 I have led 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 eight publications in formal conference/workshop proceedings, and six informal papers. Use the green download buttons to obtain the author copies.

Publications in formal conference/workshop proceedings

On Basic Feasible Functionals and the Interpretation Method, by Patrick Baillot, Ugo dal Lago, Cynthia Kop and Deivid Vale, proceedings for FoSSaCS 2024

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

Analyzing Innermost Runtime Complexity Through Tuple Interpretations, by Liye Guo and Deivid Vale, proceedings for LSFA 2022

Tuple Interpretations for Higher-Order Complexity, by Cynthia Kop and Deivid Vale, proceedings 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

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

PhD theses

Submitted to journals and conferences

• A characterization of Basic Feasible Functionals through higher-order rewriting and tuple interpretations by Patrick Baillot, Ugo dal Lago, Cynthia Kop and Deivid Vale; submitted to LMCS for the Special Issue of FoSSaCS 2024.

Project members

Cynthia Kop	Deivid Vale