Proof producing synthesis of arithmetic and cryptographic hardware

This is the homepage of the paper Proof producing synthesis of arithmetic and cryptographic hardware, authored by Konrad Slind, Scott Owens, Juliano Iyoda, and Mike Gordon. The paper appears in Formal Aspects of Computing. Here's the bibtex reference:

@article{HOLsynthesis:fac,
  author = {Konrad Slind and Scott Owens and Juliano Iyoda and Mike Gordon},
  title =  {Proof producing synthesis of arithmetic and cryptographic hardware},
  journal = {Formal Aspects of Computing},
  volume = {19}, 
  number = {3}, 
  month = {August},
  year = {2007},
  publisher = {Springer Verlag}
 }

Here is a PDF version of the paper. There is also a page collecting some of the other publications on this work.

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

Konrad Slind (on behalf of the other authors).