Cora (COnstrained Rewriting Analyser)

Cora is an analysis tool for constrained higher-order term rewriting. Cora consists of two components, both of which are in active development:

• Charlie (Constrained Higher-order Rewriting LIbrary): a Java library intended for students who want to build term rewriting tools. It supports various styles of rewriting, such as first-order, higher-order, simply-typed lambda calculus and Integer Transition Systems.
• Cora: an analysis tool to prove properties like termination or equivalence of Logically Constrained Simply-typed Term Rewriting Systems, which essentially is a simple pure functional programming language with in-built booleans and integers. The tool runs either fully automatically or with human guidance.