French version (more complete) Stéphane Glondu Research engineer - Inria Centre at Université de Lorraine VCAST CTO and co-founder - Inria Startup Studio PhD from University Paris Diderot - Paris 7 ENS Cachan alumnus Mail: firstname@lastname.net, firstname.lastname@inria.fr

Miscellaneous

• I am the main developer of Belenios;
• I am involved in the following free software project: Debian (OCaml team);
• I was involved in the following free software projects: Coq and Ocsigen;
• the scientific family tree of some acquaintances (.dot) (any additional information is welcome);
• my illustrated Erdos number (.dot);
• I used to be treasurer (2005), then network and system administrator (2005-2009) at Cr@ns;

• find a trust path to my PGP key by entering your key id:

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.
  PhD thesis, 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.

Developments in Coq

• Formalizing Coq extraction in Coq.
• Internal extraction.
• Certifying confluence in a timed process calculus, with Mehdi Dogguy.

Reports

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

Last update: 2023-10-17.