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.