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