Catherine DUBOIS 
Catherine Dubois

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

Tel:  (33) 1 69 36 73 40
Email:  catherine.dubois(at)ensiie(dot)fr
Professeur à l' Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (anciennement IIE)
Membre de l'équipe Méthodes du laboratoire Samovar depuis le 1er janvier 2016
Responsable de l'équipe Conception et Programmation Raisonnées (CPR) du laboratoire Cedric jusque juillet 2015
Collaboration INRIA dans l'équipe Deducteam
Co-responsable du pôle Vérification du GDR GPL (Génie de la programmtion et du Logiciel)
Co-responsable du groupe de travail LTP (Langages, Types et Preuves) du GDR GPL Ici jusqu'en avril 2015
Coordonnées

Recherche

Enseignement

Bibliographie

Evénements

Liens
 

 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 ) ;
    • ML with references: monomorphic type soundness ( tar file , paper )
    • 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 FoCaLiZe, projet
  • Modélisation de réglementation de sécurité dans les aéroports : projet ACI Sécurité Edemoi
  •  Evénements 

    TAP 2017 - PxTP 2017 - CP 2017 - CICM 2017 - STAF 2017 Symposium Doctoral
    TAP 2016 - CP 2016 - F-IDE 2016 - STAF 2016 Doctorial Symposium
    TAP 2015 - QRS 2015
    SETS 2015 - F-IDE 2015 (workshops FM 2015)
    TAP 2014 QSIC 2014
    TAP 2013 QSIC 2013
    Journées nationales du GDR GPL
    TAP 2009 (Test and Proof)
    TAP 2010 (Test and Proof)
    TOOLS 2010
    CSTVA 2010
    TOOLS 2011 Tutorial on Coq (in 2 parts : introduction, verification of a compiler) slides and Coq code

     Enseignements 


    Livre : Apprentissage de la programmation avec OCaml , Catherine Dubois, Valérie Ménissier Morain
     
    ENSIIE  
    Programmation fonctionnelle avec OCaml
    Programmation logique
    3A option PROG1 : sémantique des langages
    3A option PROG1 : techniques de preuve
    Validation et vérification du logiciel
    Méthodes formelles

             TSP
    MsC CCN : Test, Contracts and proofs (cours anglophone - SEFM).

              Master Paris-Saclay CILS
    Interprétation abstraite 
    Présentation de Focalize - Projet en Focalize
     

     Bibliographie 

    Liste (in)complète au format pdf

    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 . Coq code

    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 

    Une boite à outils Scilab pour l'économétrie Grocer
    Le blog de Marion
    Retour à la page d'accueil de l'ENSIIE
    Retour à la page d'accueil du Cedric