Cadence Design Systems (2012):
C-to-Silicon Compiler User's Guide.
Peter Diviànszky (2008):
Translating Imperative Algorithms to Functional Code with Unique Variable Environments.
In: Sven-Bodo Scholz: Implementation and Application of Functional Languages,
20th International Symposium, IFL 2008,
Hatfield, Hertfordshire, UK,
pp. 216–221.
John McCarthy (1962):
Towards a Mathematical Science of computation.
In: IFIP Congress,
pp. 21–28.
Magnus O. Myreen & Michael J. C. Gordon (2012):
Function Extraction.
Science of Computer Programming 77,
pp. 505–517,
doi:10.1016/j.scico.2010.10.001.
David M. Russinoff:
A Formal Theory of Register-Transfer Logic and Computer Arithmetic.
Available at http://www.russinoff.com/libman/.
David M. Russinoff, Matt Kaufmann, Eric Smith & Rob Sumners (2005):
Formal Verification of Floating-Point RTL at AMD Using the ACL2 Theorem Prover.
In: Proceeding of the 17th IMACS World Congress,
Paris.
Available at http:///www.russinoff.com/papers/paris.html.
Sol Swords & Jared Davis (2011):
Bit-Blasting ACL2 Theorems.
In: ACL2 '11,
Electronic Proceedings in Theoretical Computer Science 70,
pp. 84–102,
doi:10.4204/EPTCS.70.7.