- Curriculum Vitae -



Guillaume Gillard
32 ans 28 rue de l'échiquier 75010 Paris
Célibataire 06 60 71 60 59
Service militaire éffectué Guillaume.Gillard@laposte.net



Docteur en Informatique
Spécialité : Sémantique, Preuve et Langage



---
Expériences professionnelles Expériences universitaires Cursus Compétences Centres d'intérêts activités

---

Expériences professionnelles

2002 Consultant indépendant
  • Réalisation de modèles prospectifs sur des thématiques ressources humaines (papy
        boom et démographie) pour des grands comptes (métallurgie et caisse de retraite).
    		•
    2001-2002 Ingénieur R&D et Consultant fonctionnel au sein d'une PME
  • Rédaction d'un cahier des charges de LAD et évaluation des réponses (volet technique)
        pour une CPAM (grand compte).
  • Réalisation de modèles dynamiques (ITHINK) pour des grands comptes (aéronautique,
        distribution) et des PME (cosmétique).
  • Déploiement et gestion d'un réseau interne sous Linux (Mandrake 8.0).


    • Expériences universitaires

    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.



    • Cursus

    2001 Doctorat de Programmation de l'université Paris 7 - Denis Diderot
  • Spécialité : Sémantique, Preuve et Langage (méthodes formelles).
  • Thèse: Formalisation des langages concurrents et à objets modulo l'alpha conversion,
        sous la co-direction de Joëlle Despeyroux (INRIA) et Guy Cousineau (Paris 7).
    • 1997 DEA de Programmation : Sémantique, Preuve et Langage - Paris 7 - Denis Diderot
  • DEA commun Paris VII, Paris VI, Paris XI, Polytechnique, ENS et CNAM.
    • 1994 DEA de logique et fondements de l'informatique - Paris 7 - Denis Diderot
  • DEA de mathématiques.
    • 1993 Maîtrise de mathématiques - Paris 7 - Denis Diderot
  • Réalisée en Angleterre dans le cadre du programme d'échange ERASMUS.


    • Compétences

    Méthodes formelles
    Preuves formelles, système coq, système PVS (notions), Méthode B, sémantique des langages de programmation, langages concurrents et protocoles, types et langages de programmation, langages fonctionnels et langages à objets.
    Dynamique des systèmes
    Maîtrise des logiciels Ithink/Stella, Powersim et Vensim. Modélisations de systèmes d'information (Help Desk, gestion de projet), de systèmes de production (supply chain) et de problématiques ressources humaines (papy boom, retraites).
    Informatique
    Langages Ocaml et Scheme, Mandrake Linux (firewall, SAMBA, DNS, postfix ...), LaTex, HTML, langages (notions) Java, Turbo Pascal, ShellScript et C, MsDos et Windows 98/00, bureautique (EXCEL, WORD, POWERPOINT).
    Langues
    Anglais courant.


    Centres d'intérêts et activités

    Danse, boxe française, randonnée montagne, cinéma, bande dessinée, littérature fantastique, science fiction et roman policier.






    Mise à jour le 5 novembre 2002