Georges Gonthier

40 papers A* 10A 1B 7C 1Journal 7Unranked 13

Year	Rank	Type	Title / Venue / Authors
2016	—	`conf`	Formal Verification of Smart Contracts: Short Paper. PLAS@CCS 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
2013	B	`conf`	A Machine-Checked Proof of the Odd Order Theorem. ITP 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
2013	—	`conf`	A publication culture in software engineering (panel). ESEC/SIGSOFT FSE Steven Fraser, Luciano Baresi, Jane Cleland-Huang, Carlo A. Furia, Georges Gonthier, Paola Inverardi, Moshe Y. Vardi
2013	B	`ed.`	Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings CPP Georges Gonthier, Michael Norrish
2013	A*	`conf`	Engineering mathematics: the odd order theorem proof. POPL Georges Gonthier
2013	J	`jnl`	How to make ad hoc proof automation less ad hoc. J. Funct. Program. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2013	—	`conf`	Software engineering for mathematics (keynote). ESEC/SIGSOFT FSE Georges Gonthier
2012	B	`conf`	A Language of Patterns for Subterm Selection. ITP Georges Gonthier, Enrico Tassi
2011	B	`conf`	Advances in the Formalization of the Odd Order Theorem. ITP Georges Gonthier
2011	A	`conf`	How to make ad hoc proof automation less ad hoc. ICFP Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2011	B	`conf`	Point-Free, Set-Free Concrete Linear Algebra. ITP Georges Gonthier
2011	—	`conf`	Type design patterns for computer mathematics. TLDI Georges Gonthier
2010	J	`jnl`	An introduction to small scale reflection in Coq. J. Formaliz. Reason. Georges Gonthier, Assia Mahboubi
2009	—	`conf`	Packaging Mathematical Structures. TPHOLs François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
2009	—	`conf`	Software Engineering for Mathematics. Calculemus/MKM Georges Gonthier
2008	—	`conf`	Canonical Big Operators. TPHOLs Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
2007	—	`conf`	A Modular Formalisation of Finite Group Theory. TPHOLs Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
2007	—	`conf`	The Four Colour Theorem: Engineering of a Formal Proof. ASCM Georges Gonthier
2006	—	`ch.`	Coq. The Seventeen Provers of the World Laurent Théry, Pierre Letouzey, Georges Gonthier
2005	J	`jnl`	A hierarchy of equivalences for asynchronous calculi. J. Log. Algebraic Methods Program. Cédric Fournet, Georges Gonthier
2005	C	`conf`	Using Stålmarck's Algorithm to Prove Inequalities. ICFEM Byron Cook, Georges Gonthier
2004	B	`conf`	Choice in Dynamic Linking. FoSSaCS Martín Abadi, Georges Gonthier, Benjamin Werner
2002	J	`jnl`	Secure Implementation of Channel Abstractions. Inf. Comput. Martín Abadi, Cédric Fournet, Georges Gonthier
2000	A*	`conf`	Authentication Primitives and Their Compilation. POPL Martín Abadi, Cédric Fournet, Georges Gonthier
2000	—	`conf`	The Join Calculus: A Language for Distributed Mobile Programming. APPSEM Cédric Fournet, Georges Gonthier
1999	—	`conf`	A Top-Down Look at a Secure Message. FSTTCS Martín Abadi, Cédric Fournet, Georges Gonthier
1999	—	`conf`	Secure Communications Processing for Distributed Languages. S&P Martín Abadi, Cédric Fournet, Georges Gonthier
1998	A*	`conf`	A Hierarchy of Equivalences for Asynchronous Calculi. ICALP Cédric Fournet, Georges Gonthier
1998	A*	`conf`	Secure Implementation of Channel Abstractions. LICS Martín Abadi, Cédric Fournet, Georges Gonthier
1997	—	`conf`	Secure Implementation of Channel Abstractions. HOOTS Martín Abadi, Cédric Fournet, Georges Gonthier
1996	B	`conf`	A Calculus of Mobile Agents. CONCUR Cédric Fournet, Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, Didier Rémy
1996	A*	`conf`	The Reflexive CHAM and the Join-Calculus. POPL Cédric Fournet, Georges Gonthier
1996	A*	`conf`	Verifying the Safety of a Practical Concurrent Garbage Collector. CAV Georges Gonthier
1994	A*	`conf`	Portable, Unobtrusive Garbage Collection for Multiprocessor Systems. POPL Damien Doligez, Georges Gonthier
1992	A*	`conf`	An abstract standardisation theorem LICS Georges Gonthier, Jean-Jacques Lévy, Paul-André Melliès
1992	A*	`conf`	Linear Logic Without Boxes LICS Georges Gonthier, Martín Abadi, Jean-Jacques Lévy
1992	J	`jnl`	The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Sci. Comput. Program. Gérard Berry, Georges Gonthier
1992	A*	`conf`	The Geometry of Optimal Lambda Reduction. POPL Georges Gonthier, Martín Abadi, Jean-Jacques Lévy
1991	J	`jnl`	Incremental Development of an HDLC Entity in Esterel. Comput. Networks ISDN Syst. Gérard Berry, Georges Gonthier
1985	J	`jnl`	Algebraic Calculi of Processes and Net Expressions. Theor. Comput. Sci. Georges Gonthier