Yves Bertot : habilitation

Cette fiche réunit l'ensemble des documents que je présente pour mon habilitation à diriger des recherches.

This page gives access to the documents I presented for an "habilitation to direct research work", the last qualification necessary to become a full professor in France.

1. Un Curriculum Vitae détaillé, en date de janvier 1999. A resume in French
2. Un mémoire d'habilitation (un document de 81 pages, en français) qui synthétise l'ensemble de mes travaux de recherches. A compilation of work, much like a thesis, but smaller, which comments on all the topics covered in my research
3. Un résumé en Anglais du mémoire d'habilitation. A summary in English. (8 pages)
4. Une version électronique de mes principales publications (toutes ces publications sont en anglais). A list of publications, all of them in English. La liste de ces publications est organisée comme suit:
   • Articles publiés et soumis dans des journaux ou comme chapîtres de livres.
   1. A Canonical Calculus of Residuals in "Logical Environments", Gordon Plotkin, Gérard Huet, eds.
   2. A Generic Approach to Building User Interfaces for Theorem Provers, avec Laurent Théry, dans "Journal of symbolic computation", Vol. 25, pp. 161--194, 1998.
   3. A certified compiler for an imperative language, soumis à "Science of Computer Programming", (septembre 1998). Cet article doit encore faire l'objet de mises à jour, en particulier pour mieux le situer par rapports aux travaux existants dans ce domaine dans le monde.
   4. The CtCoq System: Design and Architecture, soumis à "Formal Aspects of Computer Science" (novembre 1998).
   • Articles publiés dans des conférences avec comité de lecture.
   1. Implementation of an Interpreter for a Parallel Language in Centaur , 3rd European Symposium on Programming, Copenhague, Denmark, LNCS 432, May 1990. Also appears as Inria Research Report no. 1076 (August 1989).
   2. Occurrences in Debugger Specifications, Proceedings of the 1991 ACM SIGPLAN Programming Language Design and Implementation (PLDI) Conference, Toronto, June 1991. Also appears as Inria Research Report no. 1350 (December 1990).
   3. Origin Functions in Lambda-calculus and Term Rewriting Systems, Proceedings of CAAP'92, Caen (France), February 1992. Also appears as Inria Research Report no. 1543 (October 1991).
   4. Real Theorem Provers Deserve Real User-Interfaces, avec Gilles Kahn et Laurent Théry, The Fifth ACM Symposium on Software Development Environments (SDE5), Washington D. C., December 1992. Also appears as Inria Research Report no. 1684 (May 1992).
   5. Proof by Pointing, avec Gilles Kahn et Laurent Théry, Symposium on Theoretical Aspects Computer Software (STACS), Sendai (Japan), LNCS 789, April 1994. Also appears as Cambridge University Research Report (December 1993).
   6. Reasoning with Executable Specifications, avec Ranan Fraer, International Joint Conference of Theory and Practice of Software Development (TAPSOFT/FASE'95) , Springer-Verlag LNCS 915, Aarhus (Denmark), May 1995.
   7. The CtCoq experience, avec Janet Bertot, User Interfaces for Theorem Provers'96, York (UK), July 1996.
   8. CtCoq: a system presentation, avec Janet Bertot, Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence, Springer-Verlag, New Brunswick, NJ, USA, July 1996
   9. Direct manipulation of Algebraic Formulae in Interactive Proof Systems , Workshop on User-Interfaces for Theorem Provers, September 1997.
   10. Head-tactics simplification Algebraic Methodology and Software Technology, volume 1349 of Lecture Notes on Computer Science, Springer Verlag, Sydney, Australia, december, 1997.
   11. Notions of dependency in proof assistants avec Olivier Pons et Laurence Rideau, Workshop on User-Interfaces for Theorem Provers, Rapport de l'université d'Eindhoven, July 1998.

Si vous voulez récupérer tous ces documents d'un seul coup, vous pouvez télécharger une archive tar

You can retrieve all these documents in one move by down-loading a tar achive.

Vous pouvez également avoir des informations supplémentaires sur mon travail en allant étudier ma page Web. You can also have a look at my personal web page.