Yves Bertot,
The CtCoq system: Design and Architecture,
Inria Report no. 3540, October 1998.
Yves Bertot and Laurent Théry,
``A Generic Approach to Building User Interfaces for Theorem Provers'',
Journal of Symbolic Computation Vol. 25, pp. 161-194, 1998.
Janet Bertot and Yves Bertot,
"CtCoq: a system presentation",
The Thirteenth International Conference on
Automated Deduction (CADE-13), New Brunswick (NJ, USA),
July 1996.
J. Bertot and Y. Bertot,
The CtCoq experience,
The International Workshop on User Interfaces for Theorem
Provers (UITP'96), York, July 1996.
Yann Coscoy, Gilles Kahn, and Laurent Théry,
``Extracting Text from Proof'',
Typed Lambda-Calculi and Applications (TLCA `95),
Springer-Verlag LNCS 905, Edimbourgh, April 1995.
Yves Bertot, Gilles Kahn, and Laurent Théry,
``Proof by Pointing'',
Symposium on Theoretical Aspects Computer Science (STACS),
Sendai (Japan), LNCS 789, Avril 1994.
Also appears as a Cambridge University Research Report (December 1993).
Laurent Théry, Yves Bertot, and Gilles Kahn,
``Real Theorem Provers Deserve Real User-Interfaces'',
The Fifth ACM Symposium on Software Development Environments (SDE5),
Washington D. C., December 1992.
Also appears as Inria Research Report no. 1684 (May 1992).
Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen, and
Francis Montagnac,
User Guide to the CtCoq Proof Environment,
February 1996.