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 seven 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

download 'Certifying Higher-Order Polynomial Interpretations', proceedings for ITP 2023
Certifying Higher-Order Polynomial Interpretations, by Niels van der Weide, Deivid Vale and Cynthia Kop, proceedings for ITP 2023
download 'Cost-Size Semantics for Call-By-Value Higher-Order Rewriting', proceedings for FSCD 2023
Cost-Size Semantics for Call-By-Value Higher-Order Rewriting, by Cynthia Kop and Deivid Vale, proceedings for FSCD 2023
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 'Analyzing Innermost Runtime Complexity Through Tuple Interpretations', proceedings for LSFA 2022
Analyzing Innermost Runtime Complexity Through Tuple Interpretations, by Liye Guo and Deivid Vale, proceedings for LSFA 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 'Complexity Analysis for Call-by-Value Higher-Order Rewriting', proceedings for WST 2023
Complexity Analysis for Call-by-Value Higher-Order Rewriting, by Cynthia Kop and Deivid Vale, proceedings for WST 2023
download 'Nijn/ONijn: A New Certification Engine for Higher-Order Termination', proceedings for HOR 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
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

Submitted to journals and conferences

Project members

Cynthia Kop Deivid Vale