François Pottier

Publication Activity (10 Years)

Years Active: 1996-2024
Publications (10 Years): 21

Top Topics

Garbage Collection

Reachability Analysis

Iris Biometrics

Top Venues

Proc. ACM Program. Lang.

Publications

François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
Thunks and Debits in Separation Logic with Time Credits. Proc. ACM Program. Lang. 8 (POPL) (2024)
Paulo Emílio de Vilhena, François Pottier
A Type System for Effect Handlers and Dynamic Labels. ESOP (2023)
Paulo Emílio de Vilhena, François Pottier
Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. Log. Methods Comput. Sci. 19 (4) (2023)
Alexandre Moine, Arthur Charguéraud, François Pottier
A High-Level Separation Logic for Heap Space under Garbage Collection. Proc. ACM Program. Lang. 7 (POPL) (2023)
Jean-Marie Madiot, François Pottier
A separation logic for heap space under garbage collection. Proc. ACM Program. Lang. 6 (POPL) (2022)
Alexandre Moine, Arthur Charguéraud, François Pottier
Specification and verification of a transient stack. CPP (2022)
Paulo Emílio de Vilhena, François Pottier
Verifying a Minimalist Reverse-Mode AD Library. CoRR (2021)
Paulo Emílio de Vilhena, François Pottier
A separation logic for effect handlers. Proc. ACM Program. Lang. 5 (POPL) (2021)
Frédéric Bour, François Pottier
Faster reachability analysis for LR(1) parsers. SLE (2021)
Glen Mével, Jacques-Henri Jourdan, François Pottier
Cosmo: a concurrent separation logic for multicore OCaml. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan
Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang. 4 (POPL) (2020)
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. ITP (2019)
Arthur Charguéraud, François Pottier
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. J. Autom. Reason. 62 (3) (2019)
Glen Mével, Jacques-Henri Jourdan, François Pottier
Time Credits and Time Receipts in Iris. ESOP (2019)
Armaël Guéneau, Arthur Charguéraud, François Pottier
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. ESOP (2018)
François Pottier
Visitors unchained. Proc. ACM Program. Lang. 1 (ICFP) (2017)
François Pottier
Verifying a hash table and its iterators in higher-order separation logic. CPP (2017)
Arthur Charguéraud, François Pottier
Temporary Read-Only Permissions for Separation Logic. ESOP (2017)
Jacques-Henri Jourdan, François Pottier
A Simple, Possibly Correct LR Parser for C11. ACM Trans. Program. Lang. Syst. 39 (4) (2017)
François Pottier
Reachability and error diagnosis in LR(1) parsers. CC (2016)
Thibaut Balabonski, François Pottier, Jonathan Protzenko
The Design and Formalization of Mezzo, a Permission-Based Programming Language. ACM Trans. Program. Lang. Syst. 38 (4) (2016)
François Pottier, Jonathan Protzenko
A Few Lessons from the Mezzo Project. SNAPL (2015)
Arthur Charguéraud, François Pottier
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. ITP (2015)
Thibaut Balabonski, François Pottier, Jonathan Protzenko
Type Soundness and Race Freedom for Mezzo. FLOPS (2014)
François Pottier
Hindley-milner elaboration in applicative style: functional pearl. ICFP (2014)
Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang
A step-indexed Kripke model of hidden state. Math. Struct. Comput. Sci. 23 (1) (2013)
François Pottier
Syntactic soundness proof of a type-and-capability system with hidden state. J. Funct. Program. 23 (1) (2013)
Armaël Guéneau, François Pottier, Jonathan Protzenko
The ins and outs of iteration in Mezzo. CoRR (2013)
Jonathan Protzenko, François Pottier
Programming with Permissions in Mezzo. CoRR (2013)
François Pottier, Jonathan Protzenko
Programming with permissions in Mezzo. ICFP (2013)
Nicolas Pouillard, François Pottier
A unified treatment of syntax with binders. J. Funct. Program. 22 (4-5) (2012)
Jacques-Henri Jourdan, François Pottier, Xavier Leroy
Validating LR(1) Parsers. ESOP (2012)
Alexandre Pilkiewicz, François Pottier
The essence of monotonic state. TLDI (2011)
François Pottier
A typed store-passing translation for general references. POPL (2011)
Nicolas Pouillard, François Pottier
A fresh look at programming with names and binders. ICFP (2010)
Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus
A Semantic Foundation for Hidden State. FoSSaCS (2010)
François Pottier
Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule. LICS (2008)
Yann Régis-Gianas, François Pottier
A Hoare Logic for Call-by-Value Functional Programs. MPC (2008)
Arthur Charguéraud, François Pottier
Functional translation of a calculus of capabilities. ICFP (2008)
Vincent Simonet, François Pottier
A constraint-based approach to guarded algebraic data types. ACM Trans. Program. Lang. Syst. 29 (1) (2007)
François Pottier
Static Name Control for FreshML. LICS (2007)
François Pottier, Yann Régis-Gianas
Towards Efficient, Typed LR Parsers. Electron. Notes Theor. Comput. Sci. 148 (2) (2006)
François Pottier, Yann Régis-Gianas
Stratified type inference for generalized algebraic data types. POPL (2006)
François Pottier, Nadji Gauthier
Polymorphic typed defunctionalization and concretization. High. Order Symb. Comput. 19 (1) (2006)
François Pottier
ml. Electron. Notes Theor. Comput. Sci. 148 (2) (2006)
Roberto Di Cosmo, François Pottier, Didier Rémy
Subtyping Recursive Types Modulo Associative Commutative Products. TLCA (2005)
François Pottier
From ML type inference to stratified type inference. ICFP (2005)
François Pottier, Christian Skalka, Scott F. Smith
A systematic approach to static access control. ACM Trans. Program. Lang. Syst. 27 (2) (2005)
François Pottier, Nadji Gauthier
Polymorphic typed defunctionalization. POPL (2004)
Nadji Gauthier, François Pottier
Numbering matters: first-order canonical forms for second-order recursive types. ICFP (2004)
François Pottier, Vincent Simonet
Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25 (1) (2003)
Jean-Christophe Filliâtre, François Pottier
Producing all ideals of a forest, functionally. J. Funct. Program. 13 (5) (2003)
Christian Skalka, François Pottier
Syntactic Type Soundness for HM(X). Electron. Notes Theor. Comput. Sci. 75 (2002)
François Pottier, Vincent Simonet
Information flow inference for ML. POPL (2002)
François Pottier
A Simple View of Type-Secure Information Flow in the p-Calculus. CSFW (2002)
Sylvain Conchon, François Pottier
JOIN(X): Constraint-Based Type Inference for the Join-Calculus. ESOP (2001)
François Pottier, Christian Skalka, Scott F. Smith
A Systematic Approach to Static Access Control. ESOP (2001)
François Pottier
Simplifying Subtyping Constraints: A Theory. Inf. Comput. 170 (2) (2001)
François Pottier
A 3-Part Type Inference Engine. ESOP (2000)
François Pottier, Sylvain Conchon
Information flow inference for free. ICFP (2000)
François Pottier
A Versatile Constraint-Based Type Inference System. Nord. J. Comput. 7 (4) (2000)
François Pottier
A Framework for Type Inference with Subtyping. ICFP (1998)
François Pottier
Simplifying Subtyping Constraints. ICFP (1996)