Je suis Charlie


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 Focal, projet
  • Modélisation de réglementation de sécurité dans les aéroports : projet ACI Sécurité Edemoi
  •  Evénements 


    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  
    Fondements de la programmation, programmation fonctionnelle avec OCaml
    Le coin des 1A IAP1 
    Le coin des 1A MLO
    Le coin des 1A IAP2 
    IPI
    3A option PR : sémantique des langages
    3A option PR : projet
    M2 LS - présentation de Focal
    Test du logiciel
    Méthodes formelles

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

              DEA d'informatique de l'Université d'Evry 
    Sémantique des langages 
    Sureté du logiciel  (Notes de cours versionps ,version pdf ), Transparents Coq pdf,
     

     Bibliographie 

    Liste 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