CRSX - Combinatory Reduction Systems with Extensions

CRSX is the Combinatory Reduction Systems with Extensions framework. It is an implementation of higher order rewriting based on Klop's Combinatory Reduction System (CRS) formalism, with a sort system that allows working with fully sorted Contraction Systems. CRSX is especially suited for developing compilers, and comes with a frontend called HACS, Higher-order Attribute Contraction Systems with special support for teaching and developing compilers. For the moment, CRSX has been used to develop compilers for medium sized languages (XQuery and JSONiq) whereas HACS is used to teach as well as implement small experimental language compilers.

CRSX is maintained in two locations:


The goals of the CRSX project (not all have been reached) are to

Everyone can use the code but if you wish to contribute then please contact the project admins.


Combinatory Reduction Systems (CRS) were invented by J. W. Klop in 1980 based on ideas in a note by Peter Aczel. The motivating idea of CRS was to allow rewriting rules that can match binding constructs and perform substitutions 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).

The CRSX project is an extended reimplementation of the Haskell program (CRSX 1) in chapter 6 of

Kristoffer H. Rose, Operational Reduction Models for Functional Programming Languages, Ph.D. thesis, DIKU, University of Copenhagen, 1996 (pdf).
The second version (CRSX 2) was part of the XQuery optimizer used in the Virtual XML project at IBM Research from 2005. The current production version (CRSX 3) was a full rewrite starting in 2007 with a compiler generator to native code used to implement the IBM DataPower appliance XQuery and JSONiq compilers.

Since 2013, CRSX development centers on CRSX 4, which integrates the HACS compiler generator frontend with the goal of supporting larger compilers.


The code is

Copyright (c) 2006, 2014 IBM Corporation.
Copyright (c) 2014, Kristoffer H. Rose.
The program and the accompanying materials are made available under the terms of the Eclipse Public License v1.0, which is included with the distribution and is available at (Older versions on SourceForge were distributed under the terms of the Common Public License v1.0,

Kristoffer H. Rose, April 6, 2014.