Simplifying Subtyping Constraints. - François Pottier (ICFP, 1996)

A Framework for Type Inference with Subtyping. - François Pottier (ICFP, 1998)

A 3-Part Type Inference Engine. - François Pottier (ESOP, 2000)

Information flow inference for free. - François Pottier; Sylvain Conchon (ICFP, 2000)

A Versatile Constraint-Based Type Inference System. - François Pottier (Nord. J. Comput., 2000)

JOIN(X): Constraint-Based Type Inference for the Join-Calculus. - Sylvain Conchon; François Pottier (ESOP, 2001)

Simplifying Subtyping Constraints: A Theory. - François Pottier (Inf. Comput., 2001)

A Simple View of Type-Secure Information Flow in the p-Calculus. - François Pottier (CSFW, 2002)

Syntactic Type Soundness for HM(X). - Christian Skalka; François Pottier (TIP@MPC, 2002)

Producing all ideals of a forest, functionally. - Jean-Christophe Filliâtre; François Pottier (J. Funct. Program., 2003)

Information flow inference for ML. - François Pottier; Vincent Simonet (ACM Trans. Program. Lang. Syst., 2003)

Numbering matters: first-order canonical forms for second-order recursive types. - Nadji Gauthier; François Pottier (ICFP, 2004)

Polymorphic typed defunctionalization. - François Pottier; Nadji Gauthier (POPL, 2004)

From ML type inference to stratified type inference. - François Pottier (ICFP, 2005)

Subtyping Recursive Types Modulo Associative Commutative Products. - Roberto Di Cosmo; François Pottier; Didier Rémy (TLCA, 2005)

An Overview of Calphaml. - François Pottier (ML, 2005)

Towards Efficient, Typed LR Parsers. - François Pottier; Yann Régis-Gianas (ML, 2005)

A systematic approach to static access control. - François Pottier; Christian Skalka; Scott F. Smith 001 (ACM Trans. Program. Lang. Syst., 2005)

Stratified type inference for generalized algebraic data types. - François Pottier; Yann Régis-Gianas (POPL, 2006)

Polymorphic typed defunctionalization and concretization. - François Pottier; Nadji Gauthier (High. Order Symb. Comput., 2006)

Static Name Control for FreshML. - François Pottier (LICS, 2007)

A constraint-based approach to guarded algebraic data types. - Vincent Simonet; François Pottier (ACM Trans. Program. Lang. Syst., 2007)

Functional translation of a calculus of capabilities. - Arthur Charguéraud; François Pottier (ICFP, 2008)

Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule. - François Pottier (LICS, 2008)

A Hoare Logic for Call-by-Value Functional Programs. - Yann Régis-Gianas; François Pottier (MPC, 2008)

A Semantic Foundation for Hidden State. - Jan Schwinghammer; Hongseok Yang; Lars Birkedal; François Pottier; Bernhard Reus (FoSSaCS, 2010)

A fresh look at programming with names and binders. - Nicolas Pouillard; François Pottier (ICFP, 2010)

A typed store-passing translation for general references. - François Pottier (POPL, 2011)

The essence of monotonic state. - Alexandre Pilkiewicz; François Pottier (TLDI, 2011)

Validating LR(1) Parsers. - Jacques-Henri Jourdan; François Pottier; Xavier Leroy (ESOP, 2012)

A unified treatment of syntax with binders. - Nicolas Pouillard; François Pottier (J. Funct. Program., 2012)

Programming with permissions in Mezzo. - François Pottier; Jonathan Protzenko (ICFP, 2013)

The ins and outs of iteration in Mezzo. - Armaël Guéneau; François Pottier; Jonathan Protzenko (CoRR, 2013)

Syntactic soundness proof of a type-and-capability system with hidden state. - François Pottier (J. Funct. Program., 2013)

A step-indexed Kripke model of hidden state. - Jan Schwinghammer; Lars Birkedal; François Pottier; Bernhard Reus; Kristian Støvring; Hongseok Yang (Math. Struct. Comput. Sci., 2013)

Type Soundness and Race Freedom for Mezzo. - Thibaut Balabonski; François Pottier; Jonathan Protzenko (FLOPS, 2014)

Hindley-milner elaboration in applicative style: functional pearl. - François Pottier (ICFP, 2014)

Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. - Arthur Charguéraud; François Pottier (ITP, 2015)

A Few Lessons from the Mezzo Project. - François Pottier; Jonathan Protzenko (SNAPL, 2015)

Reachability and error diagnosis in LR(1) parsers. - François Pottier (CC, 2016)

The Design and Formalization of Mezzo, a Permission-Based Programming Language. - Thibaut Balabonski; François Pottier; Jonathan Protzenko (ACM Trans. Program. Lang. Syst., 2016)

Verifying a hash table and its iterators in higher-order separation logic. - François Pottier (CPP, 2017)

Temporary Read-Only Permissions for Separation Logic. - Arthur Charguéraud; François Pottier (ESOP, 2017)

Visitors unchained. - François Pottier (Proc. ACM Program. Lang., 2017)

A Simple, Possibly Correct LR Parser for C11. - Jacques-Henri Jourdan; François Pottier (ACM Trans. Program. Lang. Syst., 2017)

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. - Armaël Guéneau; Arthur Charguéraud; François Pottier (ESOP, 2018)

Time Credits and Time Receipts in Iris. - Glen Mével; Jacques-Henri Jourdan; François Pottier (ESOP, 2019)

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. - Armaël Guéneau; Jacques-Henri Jourdan; Arthur Charguéraud; François Pottier (ITP, 2019)

Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. - Arthur Charguéraud; François Pottier (J. Autom. Reason., 2019)

Cosmo: a concurrent separation logic for multicore OCaml. - Glen Mével; Jacques-Henri Jourdan; François Pottier (Proc. ACM Program. Lang., 2020)

Spy game: verifying a local generic solver in Iris. - Paulo Emílio de Vilhena; François Pottier; Jacques-Henri Jourdan (Proc. ACM Program. Lang., 2020)

Faster reachability analysis for LR(1) parsers. - Frédéric Bour; François Pottier (SLE, 2021)

Verifying a Minimalist Reverse-Mode AD Library. - Paulo Emílio de Vilhena; François Pottier (CoRR, 2021)

A separation logic for effect handlers. - Paulo Emílio de Vilhena; François Pottier (Proc. ACM Program. Lang., 2021)

Specification and verification of a transient stack. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (CPP, 2022)

A separation logic for heap space under garbage collection. - Jean-Marie Madiot; François Pottier (Proc. ACM Program. Lang., 2022)

A Type System for Effect Handlers and Dynamic Labels. - Paulo Emílio de Vilhena; François Pottier (ESOP, 2023)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. - Paulo Emílio de Vilhena; François Pottier (Log. Methods Comput. Sci., 2023)

A High-Level Separation Logic for Heap Space under Garbage Collection. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (Proc. ACM Program. Lang., 2023)

Review of "Real World OCaml: Functional Programming for the Masses" Second Edition, by Yaron Minsky and Anil Madhavapeddy, 2023. - François Pottier (J. Funct. Program., 2024)

Type Inference Logics. - Denis Carnier; François Pottier; Steven Keuchel (Proc. ACM Program. Lang., 2024)

Thunks and Debits in Separation Logic with Time Credits. - François Pottier; Armaël Guéneau; Jacques-Henri Jourdan; Glen Mével (Proc. ACM Program. Lang., 2024)

Tail Modulo Cons, OCaml, and Relational Separation Logic. - Clément Allain; Frédéric Bour; Basile Clément; François Pottier; Gabriel Scherer (Proc. ACM Program. Lang., 2025)

Data Race Freedom à la Mode. - Aïna Linn Georges; Benjamin Peters; Laila Elbeheiry; Leo White; Stephen Dolan; Richard A. Eisenberg; Chris Casinghino; François Pottier; Derek Dreyer (Proc. ACM Program. Lang., 2025)

Will It Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (ACM Trans. Program. Lang. Syst., 2025)

Verified Purely Functional Catenable Real-Time Deques. - Jules Viennot; Arthur Wendling; Armaël Guéneau; François Pottier (CoRR, 2025)