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 five publications in formal conference/workshop proceedings, and four informal papers. Use the green download buttons to obtain the author copies.

Publications in formal conference/workshop proceedings

 
Analyzing Innermost Runtime Complexity Through Tuple Interpretations, by Liye Guo and Deivid Vale, proceedings for LSFA 2022 (accepted for publication)
download 'Cutting a Proof into Bite-Sized Chunks', proceedings for FSCD 2022
Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting, by Cynthia Kop, proceedings for FSCD 2022
download 'Tuple Interpretations for Higher-Order Complexity', proceedings for FSCD 2021
Tuple Interpretations for Higher-Order Complexity, by Cynthia Kop and Deivid Vale, prceedings for FSCD 2021
download 'Nominal Equational Problems', proceedings for FoSSaCS 2021
Nominal Equational Problems, by Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho and Deivid Vale, proceedings for FoSSaCS 2021
download 'Cons-free Programs and Complexity Classes between LOGSPACE and PTIME', proceedings for VPT 2020
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

download 'Tuple Interpretations and Applications to Higher-Order Runtime Complexity', proceedings for WST 2022
Tuple Interpretations and Applications to Higher-Order Runtime Complexity by Cynthia Kop and Deivid Vale, proceedings for WST 2022
download 'Nominal Disunification via Fixed-Point Constraints', proceedings for UNIF 2021
Nominal Disunification via Fixed-Point Constraints, by Leonardo M. Batista, Maribel Fernández, Daniele Nantes-Sobrinho and Deivid Vale, proceedings for UNIF 2021
download 'Formalizing higher-order termination in COQ', proceedings for WST 2021
Formalizing higher-order termination in COQ by Deivid Vale and Niels van der Weide, proceedings for WST 2021
download 'Tuple Interpretations for Higher-Order Complexity (extended abstract), proceedings for LCC 2020
Tuple Interpretations for Higher-Order Complexity (extended abstract) by Cynthia Kop and Deivid Vale, proceedings for LCC 2020

Project members

Cynthia Kop Deivid Vale