Introduction

CRS stands for Combinatory Reduction Systems, which is a powerful rewriting formalism invented by P. Aczel and J. W. Klop. The idea of CRS is to allow rewrite rules that support matching of variable binding constructs and substitution as part of rewrite steps, collectively known as higher-order rewriting.

CRSX implements CRS with a number of extension borrowed from functional programming and semantics, to facilitate using CRS for writing compilers and similar “real world” transformation systems.

The current version, described in this manual is CRSX 3, written in Java with run-time support for C.