‍

Alan Schmitt
October 22, 2021





CV





Birth: 02 April 1974 (Nancy, France)
Citizenship: French
Married, three children


Work coordinates
 ‍
Address:
INRIA Rennes – Bretagne Atlantique, Equipe-projet CELTIQUE
Campus de Beaulieu, 35042 RENNES Cedex, France
Tel:
+33 ‍(0)2 ‍99 ‍84 ‍74 ‍80.
Fax:
+33 ‍(0)2 ‍99 ‍84 ‍71 ‍71.
Email:
alan.schmitt@inria.fr
Web:
http://people.irisa.fr/Alan.Schmitt/
Home coordinates
 ‍
Address:
27 rue des Manoirs
35220 Châteaubourg, France.
Tel:
+33 ‍(0)9 ‍51 ‍79 ‍74 ‍00.
Diplomas
 ‍
2011
Habilitation à Diriger les Recherches, Université de Grenoble.
2002
Ph.D. in computer science, Ecole Polytechnique.
1999
DEA in semantics, proofs and programming. “Mention très bien”.
1998
Engineer diploma of Ecole Polytechnique (Internship Award in Applied Mathematics).
1993
Baccalauréat série E. “Mention Très bien”.
1992
American Highschool Graduation, Lincoln High School, Nebraska.
Education
 ‍
Oct 1999 – Sep 2002:
Ph.D., Moscova Project, INRIA Rocquencourt. “Conception et Implémentation de Calculs d’Agents Mobiles”. Supervisor: Jean-Jacques Lévy.
Oct 1998 – Oct 1999:
DEA in semantics, proofs and programming, University of Paris VII.
Sep 1996 – Apr 1998:
Ecole Polytechnique, major in computer science.
Aug 1991 – May 1992:
Senior highscool year, Lincoln High School, Nebraska.
Employment
 ‍
Sep 2011 – present:
Researcher at INRIA Rennes – Bretagne Atlantique, Celtique Project. Senior researcher (DR2) since October 2015.
Jan 2004 – Aug 2011:
Researcher at INRIA Rhône-Alpes, Sardes Project. Experienced researcher (CR1) since January 2005.
Sep 2007 – Aug 2008:
Sabbatical at University of Bologna, Italy, to work with Davide Sangiorgi.
Sep 2002 – Jan 2004:
Postdoc researcher at University of Pennsylvania, Philadelphia, with Benjamin Pierce, in Xtatic and Harmony projects.
Teaching
 ‍
2019 – present:
Training for Agrégation d’Informatique, ENS Rennes.
2019 – present:
Yearly course on semantics, master level, ENS Rennes.
2012 – 2018:
Yearly course on Ocaml, graduate level, INSA Rennes.
2011 – 2021:
Yearly course on formal methods for the development of safe software, graduate level, Université Rennes 1.
Jan – Apr 2011:
Course on the Coq proof assistant, post-graduate level, Université Joseph Fourier.
Feb – Apr 2010:
Course on Bisimulations and Process Calculi, post-graduate level, Université Joseph Fourier.
2010 and 2011:
Yearly course on Models of Computation, graduate level, Université Joseph Fourier.
Feb – Mar 2008:
Course on type systems and OS, graduate level, University de Bologna.

Research interests
 ‍
Programming languages and static analyses for component-based distributed systems, including type systems for process calculi and behavioral theory of distributed systems.
Formal semantics of programming languages.
Certified static analyses for secure JavaScript.
Formalization of these three research themes in the Coq proof assistant.
Refereed journal papers
 ‍
“HOπ in Coq”, with Guillaume Ambal and Sergueï Lenglet. Journal of Automated Reasoning, 2020.
“Skeletal Semantics and their Interpretations”, with Martin Bodin, Philippa Gardner, and Thomas Jensen. Proceedings of the ACM on Programming Languages, 44:1–31, 2019.
“Efficiently Deciding µ-calculus with Converse over Finite Trees”, with Pierre Genevès, Nils Gesbert, and Nabil Layaïda. ACM Transactions on Computational Logic, 2015, 16(2).
“Characterizing Contextual Equivalence in Calculi with Passivation”, with Sergueï Lenglet and Jean-Bernard Stefani. Information and Computation, November 2011, 209(11):1390–1433.
“On the Expressiveness and Decidability of Higher-Order Process Calculi”, with Ivan Lanese, Jorge A. Pérez et Davide Sangiorgi. Information and Computation, February 2011, 209(2):198–226.
“Combinators for Bi-Directional Tree Transformations: A Linguistic Approach to the View Update Problem”, with J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, and Benjamin C. Pierce. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(3):17.
“Exploiting Schemas in Data Synchronization”, with J. Nathan Foster, Michael B. Greenwald, Christian Kirkegaard, and Benjamin C. Pierce. Journal of Computer and System Sciences, 73(4), June 2007.
Lecture Notes
 ‍
“JoCaml: a Language for Concurrent Distributed and Mobile Programming”, with Fabrice Le Fessant, Cédric Fournet, and Luc Maranget. Proceedings of the 4th Summer School on Advanced Functional Programming, Oxford, 19-24 August 2002. LNCS. Springer Verlag. November 2002.
Major refereed conference papers
 ‍
“JSExplain: A Double Debugger for JavaScript”, with Arthur Charguéraud, and Thomas Wood. Proceedings of the Web Conference 2018, (April 2018).
“HOπ in Coq”, with Sergueï Lenglet. Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018) (January 2018).
“Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines” with Malgorzata Biernacka, Dariusz Bierenacki, Sergueï Lenglet, Piotr Polesiuk, and Damien Pous. Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017).
“Howe’s Method for Contextual Semantics”, with Sergueï Lenglet. Proceedings of the 26th International Conference on Concurrency Theory (Concur 2015) (September 2015).
“HOCore in Coq”, with Petar Maksimović. Proceedings of the 6th conference on Interactive Theorem Proving (ITP 2015) (August 2015).
“Expressive Logical Combinators For Free”, with Pierre Genevès. Proceedings of International Joint Conference on Artificial Intelligence (IJCAI 2015) (July 2015).
“A Trusted Mechanised JavaScript Specification”, with Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, and Gareth Smith. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014) (January 2014).
“Concurrent Flexible Reversibility”, with Ivan Lanese, Michaël Lienhardt, Claudio Antares Mezzina, and Jean-Bernard Stefani. Proceedings of the 22nd European Symposium on Programming (ESOP 2013) (March 2013).
“Controlling Reversibility in Higher-Order Pi”, with Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR 2011) (September 2011).
“Query Reasoning on Trees with Types, Interleaving, and Counting”, with Everardo Bárcenas, Pierre Genevès, and Nabil Layaïda. Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011) (July 2011).
“On the Expressiveness of Polyadic and Synchronous Communication in Higher-Order Process Calculi”, with Ivan Lanese, Jorge A. Pérez, and Davide Sangiorgi. Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP 2010) (June 2010).
“Howe’s Method for Calculi with Passivation”, with Sergueï Lenglet and Jean-Bernard Stefani. Proceedings of the 20th International Conference on Concurrency Theory (CONCUR 2009) (September 2009).
“On the Expressiveness and Decidability of Higher-Order Process Calculi”, with Ivan Lanese, Jorge A. Pérez, and Davide Sangiorgi. Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008) (June 2008).
“Boomerang: Resourceful Lenses for String Data”, with Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, and Alexandre Pilkiewicz. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08) (January 2008).

“Efficient Static Analysis of XML Paths and Types”, with Pierre Genevès and Nabil Layaïda. Proceedings of PLDI 2007 (January 2007).
“Agreeing to Agree: Conflict Resolution for Optimistically Replicated Data”, with Michael B. Greenwald, Sanjeev Khanna, Keshav Kunal, and Benjamin C. Pierce. Proceedings of 20th International Symposium on Distributed Computing (DISC 2006) (September 2006).
“Combinators for Bi-Directional Tree Transformations: A Linguistic Approach to the View Update Problem”, with J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, and Benjamin C. Pierce. Proceedings of POPL 2005 (January 2005). Most Influential POPL Paper Award, 2015.

“The M-calculus: a higher-order distributed process calculus”, with Jean-Bernard Stefani. Proceedings of POPL 2003 (January 2003).
Other publications
 ‍

http://people.rennes.inria.fr/Alan.Schmitt/publications/index.html

Software
 ‍
Necro, an ecosystem to define and manipulate formal semantics (project leader). https://skeletons.inria.fr/
JSExplain, an interactive debugger of the JavaScript Specification (developer). https://github.com/jscert/jsexplain.
JSCert, a formalization in Coq of JavaScript (developer). https://github.com/jscert/jscert.
Harmony and boomerang, bidirectional languages (collaborator). http://www.cis.upenn.edu/~bcpierce/harmony/
Unison, a file system synchronizer (collaborator). http://www.cis.upenn.edu/~bcpierce/unison/
Xtatic, an extension of C# for type safe XML manipulation (experimental, collaborator). http://www.cis.upenn.edu/~bcpierce/xtatic/
Patents
 ‍
“ Information services provision in a telecommunications network”, with Ronnie Taib and Bernard Burg. European patent EP1069792. USA patent US6512922.
Conference organization
 ‍
Programming Languages Mentoring Workshop (PLMW at POPL), 2013, 2014, and 2015.
International Symposium on Database Programming Languages (DBPL 2013) (organizer and PC co-chair).
École Jeunes Chercheurs en Programmation (EJCP) 2012, 2013, and 2014.
Vingtièmes journées francophones des langages applicatifs (JFLA 2009).
Ocaml Meeting 2009 (local organizer).
Project coordination
 ‍
Coordinator of the ANR project Ajacs (2014–2018).
Coordinator of the ANR Blanc project PiCoq (2010–2014).
Member of the steering committee for the Journées Francophones des Langages Applicatifs (JFLA) since 2010.
Coordinator of the Associated Team BACON with University of Bologna (2008).
Program committees
 ‍
Journées Francophones des Langages Applicatifs (JFLA): 2006, 2007, 2008 (vice president), 2009 (president), 2010. Types workshop: 2009. International Symposium on Database Programming Languages (DBPL): 2005, 2009, 2013 (co-chair). ACM SIGPLAN International Conference on Functional Programming (ICFP): 2008. Symposium on Trustworthy Global Computing (TGC): 2007. Programming Language Techniques for XML (PLAN-X): 2007. Types workshop: 2009. FORTE: 2015. TASE: 2017. Web Programming: 2018. ProWeb: 2018. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL): 2021. European Symposium on Programming (ESOP): 2021.
Other
 ‍
Foreign languages:
English: fluent. Italian: good notions.
Programming languages:
OCaml, Coq, JavaScript, C, Java, C#.
Competition:
Member of the team “Camls R’Us”, which came in first place in the ICFP Programming Contest 1999, and in second place in the ICFP Programming Contest 2000.

This document was translated from LATEX by HEVEA.