Janet Bertot et Yves Bertot,
"The CtCoq experience",
User Interfaces for Theorem Provers'96,
York (UK), July 1996.
Yves Bertot et Ranan Fraer,
"Reasoning with Executable Specifications",
International Joint Conference of Theory and Practice of
Software Development (TAPSOFT/FASE'95) , Springer-Verlag LNCS 915,
Aarhus (Danemark), Mai 1995.
Yves Bertot, Gilles Kahn et Laurent Théry,
``Proof by Pointing'',
Symposium on Theoretical Aspects Computer Software (STACS),
Sendai (Japon), LNCS 789, Avril 1994.
Paru également comme rapport de recherche de l'Université de
Cambridge (Décembre 1993).
Laurent Théry, Yves Bertot et Gilles Kahn,
``Real Theorem Provers Deserve Real User-Interfaces''
The Fifth ACM Symposium on Software Development Environments (SDE5),
Washington D. C., Décembre 1992.
Paru également comme rapport de recherche Inria no. 1684 (May 1992).
Yves Bertot,
``A Canonical Calculus of Residuals'',
dans Logical Environments, Gerard Huet et Gordon Plotkin, éditeurs,
Cambridge University Press, Décembre 1993.
Yves Bertot,
``Origin Functions in Lambda-calculus and Term Rewriting Systems'',
Actes de CAAP'92, Caen (France), Février 1992.
Paru également comme rapport de recherche Inria no. 1543 (Octobre 1991).
Y. Bertot,
``Occurrences in Debugger Specifications'',
Proceedings of the 1991 ACM SIGPLAN Programming Language Design and
Implementation (PLDI) Conference, Toronto, Juin 1991.
Paru également comme rapport de recherche Inria no. 1350 (Décembre
1990).
Yves Bertot,
``Implementation of an Interpreter for a Parallel Language in Centaur''
,
3rd European Symposium on Programming, Copenhague, Danemark,
LNCS 432, Mai 1990.
Paru également comme rapport de recherche Inria
no. 1076 (August 1989).