A c omputational logic. A CM Monograph, 1979. ,
A c omputational logic handbook, 1988. ,
The Coq Proof Assistant Reference Manual version 5.10. Rapport Technique 0177, 1995. ,
URL : https://hal.archives-ouvertes.fr/inria-00069994
Veriication formelle de circuits avec Coq, Journ ee du GDR-Programmation, 1994. ,
Co-inductive t ypes in Coq, Projet Coq, INRIA Rocquencourt, 1995. ,
Implementation of co-inductive t ypes in Coq: an experiment with the alternating bit protocol, 1995. ,
Why higher-order logic is a good formalism for specifying and verifying hardware, Formal Aspects of VLSI Design, 1985. ,
The Coq proof assistant -a tutorial, Available by anonymous ftp on ftp.inria.fr, 1995. ,
URL : https://hal.archives-ouvertes.fr/inria-00069993
Programming with streams in Coq. a case study : The sieve of eratosthenes, Types for Proofs and Programs, Types' 93, 1994. ,
A note on categorical data types, Category Theory and Computer Science, vol.389, 1989. ,