Compilers by Higher Order Rewriting of Terms - overview

When building compilers and other tools that manipulate programs, one is faced with a need to manipulate objects that include binders like variables and other identifiers with scope. In traditional compilers this is accomplished with some notion of structured symbol table, which then keeps track of the available names and their scope, however, when dynamically modifying the internal program this involves inventing ways to allocate fresh variables and avoid name clashes on copying, which can add significant complexity to the compiler.

In this project our goal is to reinvent compiler writing as an activity of specifying transformations of higher order abstract syntax, which should then be directly usable as the implementation of the compiler. As part of the project we are developing the transformation programmer's toolbox, which we are proposing to assist in building high quality production compilers.