Constrained Higher-Order Rewriting and Program Equivalence (CHORPE)

2021 until 2026
Project type
Software Science

CHORPE will significantly expand the theory of constrained term rewriting, and use this theoretical framework to advance the state-of-the-art in program equivalence analysis. This builds on recent advances from several international research groups, but innovates through novel uses of higher-order term rewriting.

Term rewriting is a formal system that can be used to specify algorithms. Its simple, rigorous definition makes it very suitable for formal analysis, and consequently its properties are well-studied. Higher-order term rewriting further includes anonymous functions and lambda-binders. This gives a highly liberal class of systems, which retains a simple formal foundation.

Recent studies suggest that methods from term rewriting offer a powerful tool for various subareas of program analysis. Programs in languages like C, Java and Haskell can be translated into logically constrained term rewriting systems (LCTRSs). This both provides a high-level analysis language — making the same techniques available across programming languages — and gives access to insights from a different community, backed by decades of foundational research. CHORPE aims to go further by considering constrained higher-order term rewriting. Higher-order reasoning is a natural match for object-oriented and functional languages and avoids many intrinsic limitations of previous work.

The project seeks to establish higher-order LCTRSs as a standard for both rewriting and program equivalence, by pursuing two distinct but intertwined directions of research. First, we will lay a strong theoretical foundation for higher-order constrained rewriting with several crucial analysis techniques. Second, we will devise a powerful methodology for program equivalence by translating programs in traditional languages to higher-order LCTRSs, and using rewriting-based methods to analyse them. All results will be implemented in an open-source analysis tool.

Project website

Contact information