English version Stéphane Glondu Ingénieur de recherche - Inria Nancy Grand Est - LORIA Doctorant au laboratoire PPS (Université Paris Diderot - Paris 7) Ancien élève de l'ENS Cachan Mél : prenom@nom.net, Prenom.Nom@{in,lo}ria.fr

Développements Coq

• Formalisation de l'extraction de Coq en Coq.
• Extraction interne.
• Certifying confluence in a timed process calculus, avec Mehdi Dogguy.

Publications

• Enforcing Type-Safe Linking using Inter-Package Relationships.
  Mehdi Dogguy, Stéphane Glondu, Sylvain Le Gall, and Stefano Zacchiroli.
  In JFLA 2010, La Ciotat, France, Jan 30-Feb 2, 2010.
• Extraction certifiée dans Coq-en-Coq.
  Stéphane Glondu.
  In JFLA 2009, Saint-Quentin sur Isère, France, Jan 31-Feb 3, 2009.
• DECKARD: Scalable and Accurate Tree-based Detection of Code Clones.
  Lingxiao Jiang, Ghassan Misherghi, Zhendong Su, and Stéphane Glondu.
  In Proceedings of ICSE 2007, Minneapolis, MN, USA, May 20-26, 2007.

Rapports de stage

• Garantie formelle de correction pour l'extraction Coq.
  M2 (ENS Cachan, 2007). Encadré par Pierre Letouzey (Laboratoire PPS, Université Paris Diderot-Paris 7, Paris).
• Analysis of authentication protocols.
  M1 (ENS Cachan, 2006). Encadré par Mitsuhiro Okada et Koji Hasebe (Department of Philosophy, Keio University, Tokyo).
• Uniform and non-structural subtyping. (transparents)
  L3 (Université Paris 7/ENS Cachan, 2005). Encadré par Zhendong Su (Department of Computer Science, University of California, Davis).

Divers

• je suis impliqué dans les projets de logiciel libre suivants: Coq, Ocsigen et Debian (équipe OCaml);
• l'arbre généalogique scientifique de quelques personnes de mon entourage (.dot) (toute information supplémentaire est la bienvenue);
• mon nombre de Erdos illustré (.dot);
• j'ai été trésorier (2005), puis administrateur système et réseau (2005-2009) au Cr@ns;
• mes projets dans le cadre du magistère STIC (1re année):
  • JasTeX 1.99.1: rapport - projet;
  • Carrés diaboliques: rapport - projet;
  • Compilateur Mini-Caml: rapport - projet;
  • Étude de la vitesse de convergence d'une chaîne de Markov ergodique vers sa mesure stationnaire (avec Charles Bouillaguet): rapport - projet.
• l'intégralité du cours de probabilités discrètes du magistère STIC (première année - 2004/05): pdf - sources;
• mon TIPE sur les arbres binaires de recherche équilibrés:
  • le rapport ENS;
  • les transparents;
  • le projet complet;
• la présentation sur la télévision par le réseau que j'ai faite dans le cadre du Séminaire Technique du Cr@ns (transparents - source);

• trouver des chemins de confiance vers ma clef GPG, en entrant l'id de votre clé:

Dernière mise à jour: Wed Jan 25 16:25:06 CET 2012. Site hébergé par le Cr@ns.