The Esterel synchronous programming language: Design, semantics, implementation G Berry, G Gonthier Science of computer programming 19 (2), 87-152, 1992 | 2472 | 1992 |

The synchronous approach to reactive and real-time systems A Benveniste, G Berry Proceedings of the IEEE 79 (9), 1270-1282, 1991 | 1051 | 1991 |

The reflexive CHAM and the join-calculus C Fournet, G Gonthier Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of …, 1996 | 814 | 1996 |

A calculus of mobile agents C Fournet, G Gonthier, JJ Lévy, L Maranget, D Rémy International Conference on Concurrency Theory, 406-421, 1996 | 609 | 1996 |

Formal proof–the four-color theorem G Gonthier Notices of the AMS 55 (11), 1382-1393, 2008 | 485 | 2008 |

A machine-checked proof of the odd order theorem G Gonthier, A Asperti, J Avigad, Y Bertot, C Cohen, F Garillot, S Le Roux, ... International Conference on Interactive Theorem Proving, 163-179, 2013 | 306 | 2013 |

The geometry of optimal lambda reduction G Gonthier, M Abadi, JJ Lévy Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of …, 1992 | 306 | 1992 |

Formal verification of smart contracts: Short paper K Bhargavan, A Delignat-Lavaud, C Fournet, A Gollamudi, G Gonthier, ... Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis …, 2016 | 287 | 2016 |

A small scale reflection extension for the Coq system G Gonthier, A Mahboubi, E Tassi | 251 | 2016 |

The join calculus: A language for distributed mobile programming C Fournet, G Gonthier International Summer School on Applied Semantics, 268-332, 2000 | 223 | 2000 |

Portable, unobtrusive garbage collection for multiprocessor systems D Doligez, G Gonthier Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of …, 1994 | 199 | 1994 |

A computer-checked proof of the four colour theorem G Gonthier | 193 | 2005 |

Formal proof TC Hales Notices of the AMS 55 (11), 1370-1380, 2008 | 157 | 2008 |

The four colour theorem: Engineering of a formal proof G Gonthier Asian Symposium on Computer Mathematics, 333-333, 2007 | 148 | 2007 |

Synchronous programming of reactive systems: an introduction to ESTEREL G Berry, P Couronne, G Gonthier Proceedings of the first Franco-Japanese Symposium on Programming of future …, 1988 | 148 | 1988 |

Packaging mathematical structures F Garillot, G Gonthier, A Mahboubi, L Rideau International Conference on Theorem Proving in Higher Order Logics, 327-342, 2009 | 142 | 2009 |

An introduction to small scale reflection in Coq G Gonthier, A Mahboubi | 134 | 2010 |

Linear logic without boxes G Gonthier, M Abadi, JJ Lévy LICS 92, 223-34, 1992 | 121 | 1992 |

Canonical big operators Y Bertot, G Gonthier, SO Biha, I Pasca International Conference on Theorem Proving in Higher Order Logics, 86-101, 2008 | 96 | 2008 |

A hierarchy of equivalences for asynchronous calculi C Fournet, G Gonthier International Colloquium on Automata, Languages, and Programming, 844-855, 1998 | 88 | 1998 |