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 2018 (co-chair)
Invited speaker OBT 2018 Programming and proving with FoCaLiZe: a tour from computer algebra to interoperability applications
SETS 2018 (co-chair)
Invited speaker Tetrapod (workshop@Flocs2018)

NFM 2018 - iFM 2018 - CP 2018
TAP 2017 - PxTP 2017 (chair) - 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 complète au format pdf

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


---