<page personnelle>: Catherine Dubois

Catherine DUBOIS

Catherine Dubois
ENSIIE
1, square de la résistance
91025 EVRY Cedex

Tel:	(33) 1 69 36 73 40
Email:	dubois(at)ensiie(dot)fr

Professeur à l' Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (anciennement IIE)
Responsable de l'équipe Conception et Programmation Raisonnées (CPR) du laboratoire Cedric
Actuellement en délégation à INRIA dans l'équipe Deducteam
Ancien membre de l'équipe Specif de l'Université d'Evry

Responsable du mastère spécialisé en bio-informatique de l'Institut d'Informatique d'Entreprise (site du MSBI)

Thèmes et activités de recherche

Programmation fonctionnelle
Méthodes formelles
Preuves formelles, Coq :

Propriétés du langage ML : sûreté du typage, certification de l'algorithme W (Coq theories ) ;
fonctions partielles ;
formalisation de la notion de << logique générale >>(en collaboration avec Mathieu Jaume)

Modélisation géométrique et méthodes formelles
Réutilisation de développements formels.
Développement de l'atelier Focal, projet
Modélisation de réglementation de sécurité dans les aéroports : projet ACI Sécurité Edemoi

Evénements

Journées nationales du GDR GPL

TAP 2009 (Test and Proof)

TAP 2010 (Test and Proof)

Enseignements

Apprentissage de la programmation avec OCaml

Valérie Ménissier Morain

ENSIIE (ex IIE)

Fondements de la programmation, programmation fonctionnelle avec OCaml

Le coin des 1A IAP1

Le coin des 1A MLO

Le coin des 1A IAP2

IPI

M2 LS - présentation de Focal

Test du logiciel

Méthodes formelles

DEA d'informatique de l'Université d'Evry

Sémantique des langages

Sureté du logiciel (Notes de cours versionps ,version pdf ), Transparents Coq pdf, Corrigé TPici

Bibliographie

bibliographie depuis 2000 : site Cedric

M. AIGUIER, D. BAHRAMI, C. DUBOIS, Axioms for Rewriting Theory- In Nachum Derschowitz and Claude Kirchner editors, RULE2000, Proceedings of the First International Workshop on Rule-Based Programming, 97-110,Montreal, Canada, septembre 2000.

C. DUBOIS, Un parcours de la programmation à la preuve- 2000. Habilitation à diriger des recherches, Universitéd'Evry

C. DUBOIS, ML type soundness within Coq, Theorem Proving in Higher Order Logics : 13th International Conference, TPHOLs 2000, Lecture Notes in Computer Science, vol 1869, 2000, Springer-Verlag, 126-144, Portland, Oregon, USA pdf .

C. DUBOIS, F. ROUAIX, P. WEIS.Extensional Polymorphism. Proc.of the 22nd POPL, ACM press, ACM SIGPLAN-SIGACT Symposium on PrinciplesOf Programming Languages, (1995).

C. DUBOIS, V. MÉNISSIER-MORAIN.A proved type inference tools for ML: Damas-Milner within Coq (work in progress). In J. von Wright,J. Grundy and J. Harrison, editors, Supplementary Proc. of 9th Int. Conf.Theorem Proving in Higher Order Logics, pp. 15-30, (1996).

C. DUBOIS. Sûreté du typage de ML : Spécificationet Preuve en Coq. 9èmes Journées Francophones des LangagesApplicatifs, (1998). pdf .

C. DUBOIS, V. VIGUIÉ DONZEAU-GOUGE. A step towards the mechanization of partial functions : domains as inductive predicates. CADE-15, Workshopon Mechanization of Partial Functions, (1998).pdf .

C. DUBOIS, R. GAYRAUD. Compilation de la sémantique naturelle vers ML. 10èmes Journées Francophones des Langages Applicatifs,(1999).

C. DUBOIS, V. MÉNISSIER-MORAIN.Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning,Kluwer Academic Publishers, vol 23, No 3-4, 319-346. pdf

M. JAUME, C. DUBOIS, Formalisation of general logics in the calculus of inductive constructions: Towards an abstract development to assist formal specification of logics, Research report 37-1999, LaMI,University ofEvry, 1999.

F. LEDOUX, J-M. MOTA, A. ARNOULT, C. DUBOIS, P. LE GALL, Y. BERTRAND,Spécificationsformelles du chanfreinage - In Proceedings AFADL2001, 2001. àparaître

Liens