P. Bjesse, K. Claessen, M. Sheeran, and S. Singh, Lava: Hardware Design in Haskell, Proc. ICFP, pp.174-184, 1998.

T. Braibant, Coquet: A Coq Library for Verifying Hardware, 2011.
DOI : 10.1007/s00165-007-0028-5

URL : https://hal.archives-ouvertes.fr/inria-00611757

B. Brock and W. A. Hunt-jr, The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor, Formal Methods in System Design, vol.11, issue.1, pp.71-104, 1997.
DOI : 10.1023/A:1008685826293

C. Brown and G. Hutton, Categories, allegories and circuit design, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.372-381, 1994.
DOI : 10.1109/LICS.1994.316052

S. Coupet-grimal and L. Jakubiec, Certifying circuits in type theory. Formal Asp, Comput, vol.16, issue.4, pp.352-373, 2004.

D. R. Ghica, Geometry of synthesis: a structured approach to VLSI design, Proc. POPL, pp.363-375, 2007.

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

M. Gordon, Why higher-order logic is a good formalisation for specifying and verifying hardware, 1985.

F. K. Hanna, N. Daeche, and M. Longley, Veritas+: A specification language based on type theory, Hardware Specification, Verification and Synthesis, pp.358-379, 1989.
DOI : 10.1007/0-387-97226-9_37

J. R. Harrison, A HOL Theory of Euclidean Space, Proc. TPHOLs 2005, pp.114-129, 2005.
DOI : 10.1007/11541868_8

R. Hinze, An Algebra of Scans, MPC, LNCS, pp.186-210, 2004.
DOI : 10.1007/978-3-540-27764-4_11

J. Iyoda, Translating HOL functions to hardware, 2007.

W. A. Hunt-jr and B. Brock, The Verification of a Bit-slice ALU Hardware Specification, Verification and Synthesis, LNCS, vol.408, pp.282-306, 1989.

Y. Lafont, Towards an algebraic theory of Boolean circuits, Journal of Pure and Applied Algebra, vol.184, issue.2-3, 2003.
DOI : 10.1016/S0022-4049(03)00069-0

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4

URL : https://hal.archives-ouvertes.fr/inria-00360768

T. Melham, Higher Order Logic and Hardware Verification, volume 31 of Cambridge Tracts in Theoretical Computer Science, 1993.

C. Paulin-mohring, Circuits as streams in Coq: Verification of a sequential multiplier, TYPES, pp.216-230, 1995.
DOI : 10.1007/3-540-61780-9_72

M. Sheeran, µFP, A Language for VLSI Design, LISP and Functional Programming, pp.104-112, 1984.

M. Sheeran, Hardware Design and Functional Programming: a Perfect Match, J. UCS, vol.11, issue.7, pp.1135-1158, 2005.

K. Slind, S. Owens, J. Iyoda, and M. Gordon, Proof producing synthesis of arithmetic and cryptographic hardware, Formal Aspects of Computing, vol.12, issue.1, pp.343-362, 2007.
DOI : 10.1007/s00165-007-0028-5