English version Stéphane Glondu Ingénieur de recherche - Inria Nancy Grand Est - SED Docteur en informatique (Université Paris Diderot - Paris 7) Ancien élève de l'ENS Cachan Mél : prenom@nom.net, prenom.nom@inria.fr

Divers

• je suis le développeur principal de Belenios;
• je suis membre du Club de Chiffres et des Lettres de Laxou;
• je suis trésorier de Lorraine Data Network;
• 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 PGP, en entrant l'id de votre clé:

Publications

• Distributed ElGamal a la Pedersen - Application to Helios.
  Véronique Cortier, David Galindo, Stéphane Glondu and Malika Izabachene.
  In Proceedings of the 12th annual ACM workshop on Privacy in the Electronic Society, WPES 2013, Berlin, Germany (2013) 131-142
• A generic construction for voting correctness at minimum cost - Application to Helios.
  Véronique Cortier, David Galindo, Stéphane Glondu and Malika Izabachene.
  In Cryptology ePrint Archive, Report 2013/177, 2013.
• Vers une certification de l'extraction de Coq.
  Stéphane Glondu.
  Thèse de doctorat, Université Paris Diderot, Juin 2012.
• 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.

Développements Coq

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

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).

Dernière mise à jour: 2018-05-19.