CRSX—Combinatory Reduction Systems with Extensions.

CRSX implements higher-order rewriting based on Combinatory Reduction Systems (CRS) with some extensions.
Copyright (c) 2006, 2013 IBM Corporation. All rights reserved.

This program and the accompanying materials are made available under the terms of the Common Public License v1.0, which accompanies this distribution, and is available at

For further details (including the full source code) see the CRSX SourceForge project page.

The purpose of CRSX is to implement an extended higher-order rewriting formalism to facilitate writing compilers and other syntax-directed transformation systems, specifically:


CRSX releases come in two flavors: If in doubt get the HACS release.


CRS was invented by J. W. Klop in 1980 based on ideas in a note by Peter Aczel. The foundational idea of CRS was to allow rewriting rules that allow for matching binding constructs and performing substitution as part of rewrite steps. The seminal paper on CRS is:
Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk, "Combinatory Reduction Systems: Introduction and Survey," Theoretical Computer Science 121, pp. 271-308 (1993).

Last modified: Thu Dec 12 03:13:45 EST 2013