Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

This is the homepage of the paper Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic, authored by Guodong Li, Scott Owens, and Konrad Slind. The paper appeared at ESOP 2007. Here's the bibtex reference:

@InProceedings{compilingHOL:esop07,
  author =       {G. Li and S. Owens and K. Slind},
  title =        {Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic},
  booktitle =    {European Symposium on Programming (ESOP 2007)},
  month =        {March},
  year =         2007,
  editor =       {R. de Nicola},
  series =       {Lecture Notes in Computer Science},
  volume =       {4421},
  publisher =    {Springer Verlag}
 }

Here are Postscript and PDF versions 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/sw/) directory of the distribution.

Konrad Slind (on behalf of the other authors).