Researchers

Back to the list
Share:
A A
Georges Gonthier
Former member
MSR Cambridge
Presentation

Georges Gonthier graduated from Ecole Normale Supérieure in Paris, he received his PhD from the University of Paris 11, worked at AT&T Bell laboratories for 2 years and at INRIA for 13 years.

He is presently a senior researcher at Microsoft Research Cambridge, which he joined in 2003. His work includes semantics of reactive languages, optimal reduction of functional programs, verification of concurrent memory management for Ocaml and IBM Java run-times, the join calculus model of concurrency (used in the design of Cw and Visual Basic), concurrent analysis of the Ariane 5 flight software, formal properties of security and fully computer-checked proof of the Four Colour Theorem.

Contact:
0000000000
Personal web page
Publications at the Joint Centre:

2016

Reports

titre
A Small Scale Reflection Extension for the Coq system
auteur
Georges Gonthier, Assia Mahboubi, Enrico Tassi
article
[Research Report] RR-6455, Inria Saclay Ile de France. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00258384/file/main.pdf BibTex

2013

Conference papers

titre
A Machine-Checked Proof of the Odd Order Theorem
auteur
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00816699/file/main.pdf BibTex

Books

titre
Homotopy Type Theory: Univalent Foundations of Mathematics
auteur
Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno van den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
article
Aucun, pp.448, 2013
Accès au bibtex
BibTex

2012

Conference papers

titre
A language of patterns for subterm selection
auteur
Georges Gonthier, Enrico Tassi
article
ITP, Aug 2012, Princeton, United States. pp.361-376, ⟨10.1007/978-3-642-32347-8_25⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00652286/file/rew.pdf BibTex

2011

Conference papers

titre
Point-Free, Set-Free Concrete Linear Algebra
auteur
Georges Gonthier
article
Interactive Theorem Proving - ITP 2011, Radboud University of Nijmegen, Aug 2011, Berg en Dal, Netherlands. pp.103-118, ⟨10.1007/978-3-642-22863-6_10⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00805966/file/main.pdf BibTex

2010

Journal articles

titre
An introduction to small scale reflection in Coq
auteur
Georges Gonthier, Assia Mahboubi
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2010, 3 (2), pp.95-152
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00515548/file/main-rr.pdf BibTex

2009

Conference papers

titre
Packaging Mathematical Structures
auteur
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
article
Theorem Proving in Higher Order Logics, 2009, Munich, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00368403/file/main.pdf BibTex

Reports

titre
An Ssreflect Tutorial
auteur
Georges Gonthier, Roux Stéphane Le
article
[Technical Report] RT-0367, INRIA. 2009, pp.33
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00407778/file/RT-367.pdf BibTex

2008

Conference papers

titre
Canonical Big Operators
auteur
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
article
Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. ⟨10.1007/978-3-540-71067-7⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00331193/file/main.pdf BibTex

2007

Reports

titre
A Modular Formalisation of Finite Group Theory
auteur
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
article
[Research Report] RR-6156, INRIA. 2007, pp.17
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00139131/file/RR-6156.pdf BibTex