Yves Bertot enseigne depuis 4 ans (y compris cette année 98-99) dans l'option ``Sémantique Naturelle''.
Comme l'année passée, Loïc Pottier et Laurent Théry ont donné un TD ``preuves d'algorithmes en Coq et CtCoq'', lors de la semaine intensive de novembre 98 à Sophia.
Un cours d'option ``Types et Preuves'' est proposé au DEA d'informatique de l'UNSA, auquel participe Loïc Pottier.
Loïc Pottier est chargé d'une moitié du module ``algorithmique et logique''.
Les membres du projet encadrent régulièrement des stages de DEA, maîtrise, de grandes écoles (X, ENS). De nouveaux sujets de stages sont proposés pour 1999, fondés sur les thèmes de Lemme.
Antonia Balaa et Laurent Chicli commencent leur thèse cette année, Stéphane Lavirotte entame sa troisième année, Yann Coscoy et Olivier Pons sont en fin de rédaction.
Nous prévoyons d'organiser cette année, avec la collaboration de l'ESSI (Roger Marlin), des journées d'initiation aux preuves formelles avec Coq et CtCoq, destinées à un public néophyte (ingénieurs, enseignants, chercheurs, étudiants en thèse).
Yves Bertot et Laurent Théry organisent la prochaine édition de la conférence TPHOL (Theorem Proving in Higher Order Logics) qui se tiendra en septembre 1999 à Nice. Cette conférence est le point de rencontre annuel de la communauté internationale des preuves sur machine.