Compilation as Rewriting in Higher Order Logic

This is the homepage of the paper Compilation as Rewriting in Higher Order Logic, authored by Guodong Li and Konrad Slind. The paper appeared at CADE 2007. Here's the bibtex reference:

@InProceedings{compilingHOL:esop07,
  author =       {G. Li and K. Slind},
  title =        {Compilation as Rewriting in Higher Order Logic},
  booktitle =    {Conference on Automated Deduction (CADE 2007)},
  month =        {July},
  year =         2007,
  editor =       {Frank Pfenning},
  series =       {Lecture Notes in Computer Science},
  volume =       {????},
  publisher =    {Springer Verlag}
 }

Here is a PDF version of the paper.

The compiler discussed in the paper is released with the HOL-4 implementation of higher order logic. Although this is definitely work in progress, the sources can be accessed in the (examples/dev/sw2/) directory of the distribution.

Konrad Slind.