Algebraic Calculi of Processes and Net Expressions. - Georges Gonthier (Theor. Comput. Sci., 1985)

Incremental Development of an HDLC Entity in Esterel. - Gérard Berry; Georges Gonthier (Comput. Networks ISDN Syst., 1991)

Linear Logic Without Boxes - Georges Gonthier; Martín Abadi; Jean-Jacques Lévy (LICS, 1992)

An abstract standardisation theorem - Georges Gonthier; Jean-Jacques Lévy; Paul-André Melliès (LICS, 1992)

The Geometry of Optimal Lambda Reduction. - Georges Gonthier; Martín Abadi; Jean-Jacques Lévy (POPL, 1992)

The Esterel Synchronous Programming Language: Design, Semantics, Implementation. - Gérard Berry; Georges Gonthier (Sci. Comput. Program., 1992)

Portable, Unobtrusive Garbage Collection for Multiprocessor Systems. - Damien Doligez; Georges Gonthier (POPL, 1994)

Verifying the Safety of a Practical Concurrent Garbage Collector. - Georges Gonthier (CAV, 1996)

A Calculus of Mobile Agents. - Cédric Fournet; Georges Gonthier; Jean-Jacques Lévy; Luc Maranget; Didier Rémy (CONCUR, 1996)

The Reflexive CHAM and the Join-Calculus. - Cédric Fournet; Georges Gonthier (POPL, 1996)

Secure Implementation of Channel Abstractions. - Martín Abadi; Cédric Fournet; Georges Gonthier (HOOTS, 1997)

A Top-Down Look at a Secure Message. - Martín Abadi; Cédric Fournet; Georges Gonthier (FSTTCS, 1999)

Secure Communications Processing for Distributed Languages. - Martín Abadi; Cédric Fournet; Georges Gonthier (S&P, 1999)

The Join Calculus: A Language for Distributed Mobile Programming. - Cédric Fournet; Georges Gonthier (APPSEM, 2000)

Authentication Primitives and Their Compilation. - Martín Abadi; Cédric Fournet; Georges Gonthier (POPL, 2000)

Choice in Dynamic Linking. - Martín Abadi; Georges Gonthier; Benjamin Werner (FoSSaCS, 2004)

Using Stålmarck's Algorithm to Prove Inequalities. - Byron Cook; Georges Gonthier (ICFEM, 2005)

A hierarchy of equivalences for asynchronous calculi. - Cédric Fournet; Georges Gonthier (J. Log. Algebraic Methods Program., 2005)

Coq. - Laurent Théry; Pierre Letouzey; Georges Gonthier (The Seventeen Provers of the World, 2006)

The Four Colour Theorem: Engineering of a Formal Proof. - Georges Gonthier (ASCM, 2007)

A Modular Formalisation of Finite Group Theory. - Georges Gonthier; Assia Mahboubi; Laurence Rideau; Enrico Tassi; Laurent Théry (TPHOLs, 2007)

Canonical Big Operators. - Yves Bertot; Georges Gonthier; Sidi Ould Biha; Ioana Pasca (TPHOLs, 2008)

Software Engineering for Mathematics. - Georges Gonthier (Calculemus/MKM, 2009)

Packaging Mathematical Structures. - François Garillot; Georges Gonthier; Assia Mahboubi; Laurence Rideau (TPHOLs, 2009)

An introduction to small scale reflection in Coq. - Georges Gonthier; Assia Mahboubi (J. Formaliz. Reason., 2010)

Advances in the Formalization of the Odd Order Theorem. - Georges Gonthier (ITP, 2011)

Point-Free, Set-Free Concrete Linear Algebra. - Georges Gonthier (ITP, 2011)

Type design patterns for computer mathematics. - Georges Gonthier (TLDI, 2011)

A Language of Patterns for Subterm Selection. - Georges Gonthier; Enrico Tassi (ITP, 2012)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

Engineering mathematics: the odd order theorem proof. - Georges Gonthier (POPL, 2013)

A publication culture in software engineering (panel). - Steven Fraser 001; Luciano Baresi; Jane Cleland-Huang; Carlo A. Furia; Georges Gonthier; Paola Inverardi; Moshe Y. Vardi (ESEC/SIGSOFT FSE, 2013)

Software engineering for mathematics (keynote). - Georges Gonthier (ESEC/SIGSOFT FSE, 2013)

How to make ad hoc proof automation less ad hoc. - Georges Gonthier; Beta Ziliani; Aleksandar Nanevski; Derek Dreyer (J. Funct. Program., 2013)

Formal Verification of Smart Contracts: Short Paper. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Anitha Gollamudi; Georges Gonthier; Nadim Kobeissi; Natalia Kulatova; Aseem Rastogi; Thomas Sibut-Pinote; Nikhil Swamy; Santiago Zanella-Béguelin (PLAS@CCS, 2016)