| 2023 | ESOP | A Type System for Effect Handlers and Dynamic Labels. | Paulo Emlio de Vilhena, Franois Pottier |
| 2022 | CPP | Specification and verification of a transient stack. | Alexandre Moine, Arthur Charguraud, Franois Pottier |
| 2021 | SLE | Faster reachability analysis for LR(1) parsers. | Frdric Bour, Franois Pottier |
| 2019 | ESOP | Time Credits and Time Receipts in Iris. | Glen Mvel, Jacques-Henri Jourdan, Franois Pottier |
| 2019 | ITP | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. | Armal Guneau, Jacques-Henri Jourdan, Arthur Charguraud, Franois Pottier |
| 2018 | ESOP | A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. | Armal Guneau, Arthur Charguraud, Franois Pottier |
| 2017 | CPP | Verifying a hash table and its iterators in higher-order separation logic. | Franois Pottier |
| 2017 | ESOP | Temporary Read-Only Permissions for Separation Logic. | Arthur Charguraud, Franois Pottier |
| 2016 | CC | Reachability and error diagnosis in LR(1) parsers. | Franois Pottier |
| 2015 | ITP | Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. | Arthur Charguraud, Franois Pottier |
| 2014 | FLOPS | Type Soundness and Race Freedom for Mezzo. | Thibaut Balabonski, Franois Pottier, Jonathan Protzenko |
| 2014 | ICFP | Hindley-milner elaboration in applicative style: functional pearl. | Franois Pottier |
| 2013 | ICFP | Programming with permissions in Mezzo. | Franois Pottier, Jonathan Protzenko |
| 2012 | ESOP | Validating LR(1) Parsers. | Jacques-Henri Jourdan, Franois Pottier, Xavier Leroy |
| 2011 | POPL | A typed store-passing translation for general references. | Franois Pottier |
| 2010 | FOSSACS | A Semantic Foundation for Hidden State. | Jan Schwinghammer, Hongseok Yang, Lars Birkedal, Franois Pottier, Bernhard Reus |
| 2010 | ICFP | A fresh look at programming with names and binders. | Nicolas Pouillard, Franois Pottier |
| 2008 | ICFP | Functional translation of a calculus of capabilities. | Arthur Charguraud, Franois Pottier |
| 2008 | LICS | Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule. | Franois Pottier |
| 2008 | MPC | A Hoare Logic for Call-by-Value Functional Programs. | Yann Rgis-Gianas, Franois Pottier |
| 2007 | LICS | Static Name Control for FreshML. | Franois Pottier |
| 2006 | POPL | Stratified type inference for generalized algebraic data types. | Franois Pottier, Yann Rgis-Gianas |
| 2005 | ICFP | From ML type inference to stratified type inference. | Franois Pottier |
| 2004 | ICFP | Numbering matters: first-order canonical forms for second-order recursive types. | Nadji Gauthier, Franois Pottier |
| 2004 | POPL | Polymorphic typed defunctionalization. | Franois Pottier, Nadji Gauthier |
| 2002 | POPL | Information flow inference for ML. | Franois Pottier, Vincent Simonet |
| 2001 | ESOP | JOIN(X): Constraint-Based Type Inference for the Join-Calculus. | Sylvain Conchon, Franois Pottier |
| 2001 | ESOP | A Systematic Approach to Static Access Control. | Franois Pottier, Christian Skalka, Scott F. Smith |
| 2000 | ESOP | A 3-Part Type Inference Engine. | Franois Pottier |
| 2000 | ICFP | Information flow inference for free. | Franois Pottier, Sylvain Conchon |
| 1998 | ICFP | A Framework for Type Inference with Subtyping. | Franois Pottier |
| 1996 | ICFP | Simplifying Subtyping Constraints. | Franois Pottier |