References

1. Cadence Design Systems (2012): C-to-Silicon Compiler User's Guide.
2. 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.
3. IEEE Computer Society (2011): SystemC Language Reference Manual. Available at http://homes.di.unimi.it/~pedersini/AD/SystemC_v201_LRM.pdf.
4. John McCarthy (1962): Towards a Mathematical Science of computation. In: IFIP Congress, pp. 21–28.
5. 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.
6. David M. Russinoff: A Formal Theory of Register-Transfer Logic and Computer Arithmetic. Available at http://www.russinoff.com/libman/.
7. 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.
8. 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.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org