
Georges Gonthier
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2010 – 2019
- 2016
- [c30]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
:
Formal Verification of Smart Contracts: Short Paper. PLAS@CCS 2016: 91-96 - 2013
- [j8]Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer:
How to make ad hoc proof automation less ad hoc. J. Funct. Program. 23(4): 357-401 (2013) - [c29]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:
A Machine-Checked Proof of the Odd Order Theorem. ITP 2013: 163-179 - [c28]Georges Gonthier:
Engineering mathematics: the odd order theorem proof. POPL 2013: 1-2 - [c27]Georges Gonthier:
Software engineering for mathematics (keynote). ESEC/SIGSOFT FSE 2013: 13 - [c26]Steven Fraser, Luciano Baresi
, Jane Cleland-Huang, Carlo A. Furia, Georges Gonthier, Paola Inverardi, Moshe Y. Vardi:
A publication culture in software engineering (panel). ESEC/SIGSOFT FSE 2013: 19-23 - [e1]Georges Gonthier, Michael Norrish:
Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Lecture Notes in Computer Science 8307, Springer 2013, ISBN 978-3-319-03544-4 [contents] - 2012
- [c25]Georges Gonthier, Enrico Tassi:
A Language of Patterns for Subterm Selection. ITP 2012: 361-376 - 2011
- [c24]Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer:
How to make ad hoc proof automation less ad hoc. ICFP 2011: 163-175 - [c23]Georges Gonthier:
Advances in the Formalization of the Odd Order Theorem. ITP 2011: 2 - [c22]Georges Gonthier:
Point-Free, Set-Free Concrete Linear Algebra. ITP 2011: 103-118 - [c21]Georges Gonthier:
Type design patterns for computer mathematics. TLDI 2011: 1-2 - 2010
- [j7]Georges Gonthier, Assia Mahboubi:
An introduction to small scale reflection in Coq. J. Formaliz. Reason. 3(2): 95-152 (2010)
2000 – 2009
- 2009
- [c20]Georges Gonthier:
Software Engineering for Mathematics. Calculemus/MKM 2009: 27 - [c19]François Garillot
, Georges Gonthier, Assia Mahboubi, Laurence Rideau:
Packaging Mathematical Structures. TPHOLs 2009: 327-342 - 2008
- [c18]Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca:
Canonical Big Operators. TPHOLs 2008: 86-101 - 2007
- [c17]Georges Gonthier:
The Four Colour Theorem: Engineering of a Formal Proof. ASCM 2007: 333 - [c16]Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry:
A Modular Formalisation of Finite Group Theory. TPHOLs 2007: 86-101 - 2006
- [p1]Laurent Théry, Pierre Letouzey, Georges Gonthier:
Coq. The Seventeen Provers of the World 2006: 28-35 - 2005
- [j6]Cédric Fournet, Georges Gonthier:
A hierarchy of equivalences for asynchronous calculi. J. Log. Algebraic Methods Program. 63(1): 131-173 (2005) - [c15]Byron Cook, Georges Gonthier:
Using Stålmarck's Algorithm to Prove Inequalities. ICFEM 2005: 330-344 - 2004
- [c14]Martín Abadi, Georges Gonthier, Benjamin Werner:
Choice in Dynamic Linking. FoSSaCS 2004: 12-26 - 2002
- [j5]Martín Abadi, Cédric Fournet, Georges Gonthier:
Secure Implementation of Channel Abstractions. Inf. Comput. 174(1): 37-83 (2002) - 2000
- [c13]Cédric Fournet, Georges Gonthier:
The Join Calculus: A Language for Distributed Mobile Programming. APPSEM 2000: 268-332 - [c12]Martín Abadi, Cédric Fournet, Georges Gonthier:
Authentication Primitives and Their Compilation. POPL 2000: 302-315
1990 – 1999
- 1999
- [c11]Martín Abadi, Cédric Fournet, Georges Gonthier:
A Top-Down Look at a Secure Message. FSTTCS 1999: 122-141 - [c10]Martín Abadi, Cédric Fournet, Georges Gonthier:
Secure Communications Processing for Distributed Languages. IEEE Symposium on Security and Privacy 1999: 74-88 - 1998
- [c9]Cédric Fournet, Georges Gonthier:
A Hierarchy of Equivalences for Asynchronous Calculi. ICALP 1998: 844-855 - [c8]Martín Abadi, Cédric Fournet, Georges Gonthier:
Secure Implementation of Channel Abstractions. LICS 1998: 105-116 - 1997
- [j4]Martín Abadi, Cédric Fournet, Georges Gonthier:
Secure Implementation of Channel Abstractions. Electron. Notes Theor. Comput. Sci. 10: 202-203 (1997) - 1996
- [c7]Georges Gonthier:
Verifying the Safety of a Practical Concurrent Garbage Collector. CAV 1996: 462-465 - [c6]Cédric Fournet, Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, Didier Rémy:
A Calculus of Mobile Agents. CONCUR 1996: 406-421 - [c5]Cédric Fournet, Georges Gonthier:
The Reflexive CHAM and the Join-Calculus. POPL 1996: 372-385 - 1994
- [c4]Damien Doligez, Georges Gonthier:
Portable, Unobtrusive Garbage Collection for Multiprocessor Systems. POPL 1994: 70-83 - 1992
- [j3]Gérard Berry, Georges Gonthier:
The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Sci. Comput. Program. 19(2): 87-152 (1992) - [c3]Georges Gonthier, Jean-Jacques Lévy, Paul-André Melliès:
An abstract standardisation theorem. LICS 1992: 72-81 - [c2]Georges Gonthier, Martín Abadi, Jean-Jacques Lévy:
Linear Logic Without Boxes. LICS 1992: 223-234 - [c1]Georges Gonthier, Martín Abadi, Jean-Jacques Lévy:
The Geometry of Optimal Lambda Reduction. POPL 1992: 15-26 - 1991
- [j2]Gérard Berry, Georges Gonthier:
Incremental Development of an HDLC Entity in Esterel. Comput. Networks ISDN Syst. 22(1): 35-49 (1991)
1980 – 1989
- 1985
- [j1]Georges Gonthier:
Algebraic Calculi of Processes and Net Expressions. Theor. Comput. Sci. 40: 329-337 (1985)
Coauthor Index

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
Tweets on dblp homepage
Show tweets from on the dblp homepage.
Privacy notice: By enabling the option above, your browser will contact twitter.com and twimg.com to load tweets curated by our Twitter account. At the same time, Twitter will persistently store several cookies with your web browser. While we did signal Twitter to not track our users by setting the "dnt" flag, we do not have any control over how Twitter uses your data. So please proceed with care and consider checking the Twitter privacy policy.
last updated on 2020-10-26 23:06 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint