Yves Bertot

The same page in English.

Thèmes de recherche

Cette page ne contient qu'un résumé de mes activités scientifiques. Pour une description plus complète, il vaut mieux se reporter à la page en anglais. Le thème central de mes activités de recherche est la programmation sûre, appuyée sur les systèmes de démonstration sur ordinateur. En pratique cet objectif se décompose en quatre grands domaines:

Environnements de travail pour les systèmes de démonstration sur ordinateur: les systèmes CtCoq et Pcoq.
Amélioration des systèmes de démonstration basés sur la théorie des types. En particulier, je cherche à améliorer les outils qui permettent de raisonner sur les fonctions récursives bien fondées et à rendre les raisonnements moins dépendants des choix de structures de données.
Démonstrations de correction pour des outils de programmation. Ces travaux nécessitent la description des langages de programmation dans le langage des systèmes de démonstration sur ordinateur.
Démonstration de correction pour des algorithmes généraux: algorithmes d'arithmétique des ordinateurs et algorithmes de géométrie.

Enseignement

Je donne un cours de sémantique des langages de programmation en maitrise. Vous pouvez accéder aux notes de ce cours.

Je donne un cours de preuve en Coq en DEA. Vous pouvez accéder aux transparents de ce cours.

J'ai également eu l'occasion de donner une introduction pour un cours de méthodes formelles en DESS. Voici les notes que j'ai rédigées pour ce cours.

Publications

livre sur Coq.

ce lien

personnalités et organisations

Référence rapide aux outils