R. S. Boyer and J. S. Moore, A c omputational logic. A CM Monograph, 1979.

R. S. Boyer and J. S. Moore, A c omputational logic handbook, 1988.

C. Cornes, J. Courant, J. Filli^-atre, G. Huet, P. Manoury et al., The Coq Proof Assistant Reference Manual version 5.10. Rapport Technique 0177, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00069994

S. Coupet-grimal and L. Jakubiec, Veriication formelle de circuits avec Coq, Journ ee du GDR-Programmation, 1994.

E. Gim, Co-inductive t ypes in Coq, Projet Coq, INRIA Rocquencourt, 1995.

E. Gim, Implementation of co-inductive t ypes in Coq: an experiment with the alternating bit protocol, 1995.

M. Gordon, Why higher-order logic is a good formalism for specifying and verifying hardware, Formal Aspects of VLSI Design, 1985.

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq proof assistant -a tutorial, Available by anonymous ftp on ftp.inria.fr, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00069993

F. Leclerc and C. Paulin-mohring, Programming with streams in Coq. a case study : The sieve of eratosthenes, Types for Proofs and Programs, Types' 93, 1994.

G. C. Wraith, A note on categorical data types, Category Theory and Computer Science, vol.389, 1989.