Constrained Higher-Order Rewriting and Program Equivalence (CHORPE)

From February 2021 to January 2026 I have led the NWO VIDI project Constrained Higher-Order Rewriting and Program Equivalence, grant number VI.Vidi.193.075. This page list the work performed as part of this project.

Project goals

The goal of CHORPE is to study program equivalence through translations to logically constrained term rewriting systems. Our particular focus is to translate higher-order features and use the knowledge of higher-order term rewriting analysis from the rewriting community.

Collaborations

We have started the TEA seminar, an online seminar uniting groups in Nijmegen, Amsterdam and Nagoya who all work on equivalence of and through term rewriting.

Publications

To date, the project has resulted in seven publications in formal conference proceedings, and six informal papers documenting work in progress. Use the green download buttons to obtain the author copies.

Publications in formal conference proceedings

An Innermost DP Framework for Constrained Higher-Order Rewriting, by Carsten Fuhs, Liye Guo and Cynthia Kop, proceedings for FSCD 2025

Rewriting induction for higher-order constrained term rewriting systems, by Kasper Hagens and Cynthia Kop, proceedings for LOPSTR 2024

Higher-Order Constrained Dependency Pairs for (Universal) Computability, by Liye Guo, Kasper Hagens, Cynthia Kop and Deivid Vale, proceedings for MFCS 2024

Higher-Order LCTRSs and Their Termination, by Liye Guo and Cynthia Kop, proceedings for ESOP 2024

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

Publications in informal workshop proceedings

Bounded Rewriting Induction for LCTRSs, by Kasper Hagens and Cynthia Kop, proceedings for WPTE 2025

Higher-order inductive theorems via recursor templates, by Kasper Hagens and Cynthia Kop, proceedings for HOR 2025

Higher-order LCTRSs and their termination, by Liye Guo and Cynthia Kop, proceedings for HOR 2023

Matrix invariants for program equivalence in LCTRSs, by Kasper Hagens and Cynthia Kop, proceedings for WPTE 2023

A transitive HORPO for curried systems by Liye Guo and Cynthia Kop, proceedings for WST 2022

Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems by Wouter Brozius, Kasper Hagens and Cynthia Kop, proceedings for WPTE 2022

Submitted to conferences and journals

• A characterization of basic feasible functionals through higher-order rewriting and tuple interpretations, by Patrick Baillot, Ugo dal Lago, Cynthia Kop and Deivid Vale, accepted for the LMCS special issue of FoSSaCS 2024

Project members

Cynthia Kop	Liye Guo	Kasper Hagens	Deivid Vale