Translating HOL functions to hardware
University of Cambridge, University of Utah
How it's done [
postcript
|
pdf
]
(TPHOLs 2005 "Emerging Trends")
Shorter paper [
postcript
|
pdf
]
(
AVoCS 2005
)
DCC'06
contribution:
Proof producing synthesis of arithmetic and cryptographic hardware
(includes a
FAQ
)
Automatic Formal Synthesis of Hardware from Higher Order Logic
(
ENTCS, Vol. 145, 2006
)
Tail-recursive multiplier example
Factorial example
Code repository
Compiler README
Page by
Juliano Iyoda
on
downloading to the FPGA board
(uses some ML developed by
Ken Friis Larsen
)
Page maintained by Mike Gordon (some links known to be broken)
