A compiler from Higher Order Logic to hardware (with a detailed survey of the field)

Related projects for other languages:

Scheme: http://scheme2006.cs.uchicago.edu/05-saint-mleux.pdf

Haskell: http://www-users.cs.york.ac.uk/~mfn/reduceron/