| 2000 - 2001 |
Enseignant chercheur (ATER) au département informatique de l'université de NANTES |
|
| Recherche |
Formalisation et preuve de correction du typage du pi-calcul en coq. |
| Enseignements |
Programmation fonctionnelle (Ocaml).
Programmation impérative (PASCAL).
Algorithmique. |
|
| 1997 - 2000 |
Doctorant au sein des laboratoires CROAP puis Certilab de l' INRIA Sophia Antipolis |
|
| Recherche |
Développement d'une méthode de formalisation des langages de
programmation pour les outils de manipulation de preuves formelles.
Application dans le système coq sur un calcul concurrent à objets.
Présentation de l'implémentation en coq lors d'une conférence (CADE-17)
aux USA et présentation de la méthode à un workshop en Suède.
|
| Enseignements |
Programmation fonctionnelle (Scheme).
Programmation impérative et objet (C, Java).
Systèmes d'exploitation (LINUX, MsDos).
Outils formels et mathématiques pour l'informatique.
Bureautique (EXCEL). |
|
| 1997 |
Stage de DEA de 6 mois au sein du laboratoire CROAP de l' INRIA Sophia Antipolis |
|
| Recherche |
Spécification d'un compilateur Mini-ML en typol (prolog) et preuve
formelle de correction avec l'outil coq.
|
|
| 1994 - 1996 |
Enseignant (coopérant du service national) en mathématiques à l'université de Bangui (RCA) |
|
| Charges |
Responsable des enseignements en mathématiques de la première
année de l'université des sciences (200 étudiants, 5 enseignants).
|
| Enseignements |
Mathématiques pour les premières et deuxièmes années des cursus
scientifiques.
|
|
| 1994 |
Stage de 6 mois au sein du laboratoire de logique de l'université Paris 7 - Denis Diderot |
|
| Recherche |
Etude sémantique de formules logiques restreintes du deuxième ordre.
|
|
| 1993 |
Séjour de 9 mois au département de mathématiques de l'université de Leeds (Angleterre). |
|
| Formation |
Maîtrise de mathématique. options : logique et algèbre.
|
|
