???global.info.a_carregar???
François Pottier is a senior researcher (DR1) at Inria in Paris, France. Since 2019, he has been the head of the Cambium team, home of the OCaml programming language. He is broadly interested in the theory and implementation of programming languages. More specifically, he has expertise in the syntax, semantics, parsing, and compilation of programming languages; in the design, metatheory and implementation of type systems; and in the field of program verification using Separation Logic. With his co-authors, he has recently proposed several extensions of the Iris logic to reason about time complexity, about space complexity in the presence of garbage collection, and about effect handlers. He is the author of approximately 65 papers in international conferences and journals. He is the author of several libraries and tools in the OCaml ecosystem. The best known and most important of these is the Menhir parser generator, which arguably is one of the most advanced and feature-rich LR parser generators in the world. He currently supervises or has supervised 15 PhD students. He has taught at École Polytechnique, where he was an associate professor (2004-2016). He currently teaches a master's course at Université Paris Cité. He has worked for the company Trusted Logic (1998-1999), where he developed an optimizing translator of Java into JavaCard. He holds a patent for this tool. He has been a member of the program committee for over 12 international conferences and a chair of the program committee for two international conferences (ICFP 2019 and POPL 2023). He has been an associate editor for the journals TOPLAS and JFP. He is a member of the IFIP working groups 2.8 (functional programming) and 2.16 (language design). The broad aim of François Pottier's current research is to make program specification and verification a reality, both for verification experts and for professional programmers. He is involved in the design of Gospel, a formal specification language for OCaml. He also leads a project to develop a formal semantics of OCaml and use it as a basis to apply the state-of-the-art logic Iris to the verification of OCaml programs.
Read full resume ↓
Identification

Personal identification

Full name
François Pottier

Citation names

  • Pottier, François

Author identifiers

Ciência ID
E818-30C1-4D6F
ORCID iD
0000-0002-4069-1235
Google Scholar ID
https://scholar.google.com/citations?user=7R6jcZ0AAAAJ&hl=fr

Websites

Knowledge fields

  • Exact Sciences - Computer and Information Sciences - Computer Sciences

Languages

Language Speaking Reading Writing Listening Peer-review
French (Mother tongue)
English Proficiency (C2) Proficiency (C2) Proficiency (C2) Proficiency (C2) Proficiency (C2)
Education
Degree Classification
1998/07/03
Concluded
 Thèse de doctorat en informatique (Doktor (PhD))
Université Paris Cité, France
"SYNTHÈSE DE TYPES EN PRÉSENCE DE SOUS-TYPAGE : DE LA THÉORIE À LA PRATIQUE" (THESIS/DISSERTATION)
Affiliation

Science

Category
Host institution 		Employer
1999/09/01 - Current Researcher (Research) Inria Centre de Recherche de Paris, France
Outputs

Publications

Book chapter
  1. François Pottier; Didier Rémy; Benjamin C. Pierce. "The Essence of ML Type Inference". edited by Benjamin C. Pierce, 389-489. MIT Press, 2005.
Conference paper
  1. Paulo Emílio de Vilhena; François Pottier. "A Type System for Effect Handlers and Dynamic Labels". 2023.
  2. Alexandre Moine; Arthur Charguéraud; François Pottier. "Specification and verification of a transient stack". 2022.
    10.1145/3497775.3503677
  3. Frédéric Bour; François Pottier. "Faster Reachability Analysis for LR(1) Parsers". 2021.
    https://doi.org/10.1145/3486608.3486903
  4. François Pottier. "Strong Automated Testing of OCaml Libraries". 2021.
  5. Armaël Guéneau; Jacques-Henri Jourdan; Arthur Charguéraud; François Pottier; John Harrison; John O'Leary; Andrew Tolmach. "Formal Proof and Analysis of an Incremental Cycle Detection Algorithm". 2019.
  6. Glen Mével; Jacques-Henri Jourdan; François Pottier; Luis Caires. "Time credits and time receipts in Iris". 2019.
  7. Armaël Guéneau; Arthur Charguéraud; François Pottier; Amal Ahmed. "A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification". 2018.
  8. François Pottier. "Visitors Unchained". 2017.
  9. Arthur Charguéraud; François Pottier; Hongseok Yang. "Temporary Read-Only Permissions for Separation Logic". 2017.
  10. François Pottier. "Verifying a hash table and its iterators in higher-order separation logic". 2017.
    https://doi.org/10.1145/3018610.3018624
  11. François Pottier. "Reachability and error diagnosis in LR(1) parsers". 2016.
    http://dx.doi.org/10.1145/2892208.2892224
  12. François Pottier. "Reachability and error diagnosis in LR(1) automata". 2016.
  13. Arthur Charguéraud; François Pottier. "Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation". 2015.
  14. François Pottier; Jonathan Protzenko; Thomas Ball; Rastislav Bodik; Shriram Krishnamurthi; Benjamin S. Lerner; Greg Morrisett. "A few lessons from the Mezzo project". 2015.
  15. François Pottier. "Depth-First Search and Strong Connectivity in Coq". 2015.
  16. François Pottier. "Hindley-Milner elaboration in applicative style". 2014.
    http://dx.doi.org/10.1145/2628136.2628145
  17. Thibaut Balabonski; François Pottier; Jonathan Protzenko. "Type Soundness and Race Freedom for Mezzo". 2014.
  18. François Pottier; Jonathan Protzenko. "Programming with permissions in Mezzo". 2013.
    http://dx.doi.org/10.1145/2500365.2500598
  19. Jacques-Henri Jourdan; François Pottier; Xavier Leroy. "Validating LR(1) Parsers". 2012.
  20. François Pottier. "A typed store-passing translation for general references". 2011.
    http://dx.doi.org/10.1145/1925844.1926403
  21. Alex; re Pilkiewicz; François Pottier. "The essence of monotonic state". 2011.
    http://dx.doi.org/10.1145/1929553.1929565
  22. Nicolas Pouillard; François Pottier. "A fresh look at programming with names and binders". 2010.
    http://doi.acm.org/10.1145/1863543.1863575
  23. Jan Schwinghammer; Hongseok Yang; Lars Birkedal; François Pottier; Bernhard Reus; C.-H. L. Ong. "A Semantic Foundation for Hidden State". 2010.
  24. Arthur Charguéraud; François Pottier. "Functional Translation of a Calculus of Capabilities". 2008.
    http://doi.acm.org/10.1145/1411204.1411235
  25. Yann Régis-Gianas; François Pottier. "A Hoare Logic for Call-by-Value Functional Programs". 2008.
  26. François Pottier. "Hiding local state in direct style: a higher-order anti-frame rule". 2008.
  27. François Pottier. "Static Name Control for FreshML". 2007.
  28. François Pottier; Yann Régis-Gianas. "Towards efficient, typed LR parsers". 2006.
  29. François Pottier. "An overview of Caml". 2006.
  30. François Pottier; Yann Régis-Gianas. "Stratified type inference for generalized algebraic data types". 2006.
    http://doi.acm.org/10.1145/1111037.1111058
  31. Roberto Di Cosmo; François Pottier; Didier Rémy. "Subtyping Recursive Types modulo Associative Commutative Products". 2005.
  32. Nadji Gauthier; François Pottier. "Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types". 2004.
    http://doi.acm.org/10.1145/1016850.1016872
  33. François Pottier; Nadji Gauthier. "Polymorphic Typed Defunctionalization". 2004.
    http://doi.acm.org/10.1145/964001.964009
  34. François Pottier. "A Constraint-Based Presentation and Generalization of Rows". 2003.
  35. Christian Skalka; François Pottier. "Syntactic Type Soundness for HM(X)". 2002.
  36. François Pottier. "A Simple View of Type-Secure Information Flow in the p-Calculus". 2002.
  37. François Pottier; Vincent Simonet. "Information Flow Inference for ML". 2002.
    http://doi.acm.org/10.1145/503272.503302
  38. Sylvain Conchon; François Pottier; David S; s. "JOIN$(X)$: Constraint-Based Type Inference for the Join-Calculus". 2001.
  39. François Pottier; Christian Skalka; Scott Smith; David S; s. "A Systematic Approach to Static Access Control". 2001.
  40. François Pottier; Sylvain Conchon. "Information Flow Inference for Free". 2000.
    http://doi.acm.org/10.1145/351240.351245
  41. François Pottier; Gert Smolka. "A 3-part type inference engine". 2000.
  42. François Pottier. "A Framework for Type Inference with Subtyping". 1998.
    http://doi.acm.org/10.1145/289423.289448
  43. François Pottier. "Simplifying subtyping constraints". 1996.
    http://doi.acm.org/10.1145/232627.232642
Journal article
  1. Alexandre Moine; Arthur Charguéraud; François Pottier. "A High-Level Separation Logic for Heap Space under Garbage Collection". Proceedings of the ACM on Programming Languages (2023): https://doi.org/10.1145/3571218.
    10.1145/3571218
  2. Jean-Marie Madiot; François Pottier. "A separation logic for heap space under garbage collection". Proceedings of the ACM on Programming Languages (2022): https://doi.org/10.1145/3498672.
    10.1145/3498672
  3. Paulo Emílio de Vilhena; François Pottier. "A Separation Logic for Effect Handlers". Proceedings of the ACM on Programming Languages 5 POPL (2021): http://cambium.inria.fr/~fpottier/publis/de-vilhena-pottier-sleh.pdf.
  4. Glen Mével; Jacques-Henri Jourdan; François Pottier. "Cosmo: A Concurrent Separation Logic for Multicore OCaml". Proceedings of the ACM on Programming Languages 4 ICFP (2020): http://cambium.inria.fr/~fpottier/publis/mevel-jourdan-pottier-cosmo-2020.pdf.
  5. Paulo Emílio de Vilhena; François Pottier; Jacques-Henri Jourdan. "Spy Game: Verifying a Local Generic Solver in Iris". Proceedings of the ACM on Programming Languages 4 POPL (2020): http://cambium.inria.fr/~fpottier/publis/de-vilhena-pottier-jourdan-spy-game-2020.pdf.
  6. Arthur Charguéraud; François Pottier. "Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits". Journal of Automated Reasoning 62 3 (2019): 331-365. http://cambium.inria.fr/~fpottier/publis/chargueraud-pottier-uf-sltc.pdf.
  7. Jacques-Henri Jourdan; François Pottier. "A simple, possibly correct LR parser for C11". ACM Transactions on Programming Languages and Systems 39 4 (2017): 14:1-14:36. http://cambium.inria.fr/~fpottier/publis/jourdan-fpottier-2016.pdf.
  8. Thibaut Balabonski; François Pottier; Jonathan Protzenko. "The Design and Formalization of Mezzo, a Permission-Based Programming Language". ACM Transactions on Programming Languages and Systems 38 4 (2016): 14:1-14:94. http://cambium.inria.fr/~fpottier/publis/bpp-mezzo-journal.pdf.
    http://dx.doi.org/10.1145/2837022
  9. Jan Schwinghammer; Lars Birkedal; François Pottier; Bernhard Reus; Kristian Støvring; Hongseok Yang. "A step-indexed Kripke Model of Hidden State". Mathematical Structures in Computer Science 23 1 (2013): 1-54. http://cambium.inria.fr/~fpottier/publis/sikmhs.pdf.
  10. François Pottier. "Syntactic soundness proof of a type-and-capability system with hidden state". Journal of Functional Programming 23 1 (2013): 38-144. http://cambium.inria.fr/~fpottier/publis/fpottier-ssphs.pdf.
  11. Nicolas Pouillard; François Pottier. "A unified treatment of syntax with binders". Journal of Functional Programming 22 4--5 (2012): 614-704. http://cambium.inria.fr/~fpottier/publis/pouillard-pottier-unified.pdf.
  12. Vincent Simonet; François Pottier. "A Constraint-Based Approach to Guarded Algebraic Data Types". ACM Transactions on Programming Languages and Systems 29 1 (2007): http://cambium.inria.fr/~fpottier/publis/simonet-pottier-hmg-toplas.pdf.
    http://doi.acm.org/10.1145/1180475.1180476
  13. François Pottier; Nadji Gauthier. "Polymorphic Typed Defunctionalization and Concretization". Higher-Order and Symbolic Computation 19 (2006): 125-162. http://cambium.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf.
  14. François Pottier; Christian Skalka; Scott Smith. "A Systematic Approach to Static Access Control". ACM Transactions on Programming Languages and Systems 27 2 (2005): 344-382. http://cambium.inria.fr/~fpottier/publis/fpottier-skalka-smith-toplas.pdf.
    http://doi.acm.org/10.1145/1057387.1057392
  15. Jean-Christophe Filliâtre; François Pottier. "Producing All Ideals of a Forest, Functionally". Journal of Functional Programming 13 5 (2003): 945-956. http://cambium.inria.fr/~fpottier/publis/filliatre-pottier.pdf.
  16. François Pottier; Vincent Simonet. "Information Flow Inference for ML". ACM Transactions on Programming Languages and Systems 25 1 (2003): 117-158. http://cambium.inria.fr/~fpottier/publis/fpottier-simonet-toplas.pdf.
    http://doi.acm.org/10.1145/596980.596983
  17. François Pottier. "Simplifying subtyping constraints: a theory". Information & Computation 170 2 (2001): 153-183. http://cambium.inria.fr/~fpottier/publis/fpottier-ic01.pdf.
  18. François Pottier. "A Versatile Constraint-Based Type Inference System". Nordic Journal of Computing 7 4 (2000): 312-347. http://cambium.inria.fr/~fpottier/publis/fpottier-njc-2000.pdf.
Report
  1. François Pottier. 1998. Type inference in the presence of subtyping: from theory to practice. http://hal.inria.fr/docs/00/07/32/05/PDF/RR-3483.pdf.
  2. Michel Mauny; François Pottier. 1993. An implementation of Caml Light with existential types. http://cambium.inria.fr/~fpottier/publis/rapport-maitrise.pdf.
Thesis / Dissertation
  1. "Synthèse de types en présence de sous-typage: de la théorie à la pratique". 1998. http://cambium.inria.fr/~fpottier/publis/these-fpottier.pdf.

Other

Software
  1. FrançoisPottier; Yann Régis-Gianas. "Menhir". Inria Centre de Recherche de Paris. 2005.
Activities

Supervision

Thesis Title
Role 		Degree Subject (Type)
Institution / Organization
2022/09/01 - Current (thesis is still ongoing; title to be determined)
Supervisor of Clément Allain
2021/09/01 - Current (thesis is still ongoing; title to be determined)
Supervisor of Alexandre Moine
2020/12/01 - Current (thesis is still ongoing; title to be determined)
Co-supervisor of Olivier Martinot
2019/10/01 - Current (thesis is still ongoing, title to be determined)
Supervisor of Frédéric Bour
2019/09/01 - 2022/12/01 Proof of Programs with Effect Handlers
Supervisor of Paulo Emílio de Vilhena
2018/11/01 - 2022/12/01 A mechanized program logic for concurrent programs with the weak memory model of Multicore OCaml
Supervisor of Glen Mével
2016/09/01 - 2019/12/01 Mechanized Verification of the Correctness and Asymptotic Complexity of Programs
Supervisor of Armaël Guéneau
2017/01/01 - 2019/07/01 (thesis was not defended)
Supervisor of Naomi Testard
2010/09/01 - 2014/09/01 Mezzo, the language of the future
Supervisor of Jonathan Protzenko
2008/03/01 - 2012/01/01 Namely, Painless: A unifying approach to safe programming with first-order syntax with binders
Supervisor of Nicolas Pouillard
2008/12/01 - 2011/06/01 (thesis was not defended)
Supervisor of Alexandre Pilkiewicz
2007/09/01 - 2010/12/01 Characteristic Formulae for Mechanized Program Verification
Supervisor of Arthur Charguéraud
2004/09/01 - 2007/11/01 From types to logical assertions : automatic or assisted proofs of property about functional programs
Supervisor of Yann Régis-Gianas
2003/09/01 - 2006/01/01 (thesis was not defended)
Supervisor of Nadji Gauthier
2001/03/01 - 2004/03/01 Inférence de flots d'information pour ML: formalisation et implantation
Supervisor of Vincent Simonet

Conference scientific committee

Conference name Conference host
2023/01/15 - 2023/01/23 POPL 2023 Andrew Myers
2019/08/18 - 2019/08/23 ICFP 2019 Derek Dreyer (general chair)