François Pottier

73 papers A* 6A 17B 8Misc 1Journal 32Unranked 7

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Data Race Freedom à la Mode. Proc. ACM Program. Lang. Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer
2025	J	`jnl`	Formal Semantics and Program Logics for a Fragment of OCaml. Proc. ACM Program. Lang. Remy Seassau, Irene Yoon, Jean-Marie Madiot, François Pottier
2025	J	`jnl`	Tail Modulo Cons, OCaml, and Relational Separation Logic. Proc. ACM Program. Lang. Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer
2025	J	`jnl`	Verified Purely Functional Catenable Real-Time Deques. CoRR Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier
2025	J	`jnl`	Will It Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection. ACM Trans. Program. Lang. Syst. Alexandre Moine, Arthur Charguéraud, François Pottier
2024	J	`jnl`	Review of "Real World OCaml: Functional Programming for the Masses" Second Edition, by Yaron Minsky and Anil Madhavapeddy, 2023. J. Funct. Program. François Pottier
2024	J	`jnl`	Tail Modulo Cons, OCaml, and Relational Separation Logic. CoRR Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer
2024	J	`jnl`	Thunks and Debits in Separation Logic with Time Credits. Proc. ACM Program. Lang. François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
2024	J	`jnl`	Type Inference Logics. Proc. ACM Program. Lang. Denis Carnier, François Pottier, Steven Keuchel
2023	J	`jnl`	A High-Level Separation Logic for Heap Space under Garbage Collection. Proc. ACM Program. Lang. Alexandre Moine, Arthur Charguéraud, François Pottier
2023	A	`conf`	A Type System for Effect Handlers and Dynamic Labels. ESOP Paulo Emílio de Vilhena, François Pottier
2023	J	`jnl`	Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. Log. Methods Comput. Sci. Paulo Emílio de Vilhena, François Pottier
2022	J	`jnl`	A separation logic for heap space under garbage collection. Proc. ACM Program. Lang. Jean-Marie Madiot, François Pottier
2022	B	`conf`	Specification and verification of a transient stack. CPP Alexandre Moine, Arthur Charguéraud, François Pottier
2021	J	`jnl`	A separation logic for effect handlers. Proc. ACM Program. Lang. Paulo Emílio de Vilhena, François Pottier
2021	B	`conf`	Faster reachability analysis for LR(1) parsers. SLE Frédéric Bour, François Pottier
2021	J	`jnl`	Verifying a Minimalist Reverse-Mode AD Library. CoRR Paulo Emílio de Vilhena, François Pottier
2020	J	`jnl`	Cosmo: a concurrent separation logic for multicore OCaml. Proc. ACM Program. Lang. Glen Mével, Jacques-Henri Jourdan, François Pottier
2020	J	`jnl`	Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang. Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan
2019	B	`conf`	Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. ITP Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
2019	A	`conf`	Time Credits and Time Receipts in Iris. ESOP Glen Mével, Jacques-Henri Jourdan, François Pottier
2019	J	`jnl`	Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. J. Autom. Reason. Arthur Charguéraud, François Pottier
2018	A	`conf`	A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. ESOP Armaël Guéneau, Arthur Charguéraud, François Pottier
2017	J	`jnl`	A Simple, Possibly Correct LR Parser for C11. ACM Trans. Program. Lang. Syst. Jacques-Henri Jourdan, François Pottier
2017	A	`conf`	Temporary Read-Only Permissions for Separation Logic. ESOP Arthur Charguéraud, François Pottier
2017	B	`conf`	Verifying a hash table and its iterators in higher-order separation logic. CPP François Pottier
2017	J	`jnl`	Visitors unchained. Proc. ACM Program. Lang. François Pottier
2016	B	`conf`	Reachability and error diagnosis in LR(1) parsers. CC François Pottier
2016	J	`jnl`	The Design and Formalization of Mezzo, a Permission-Based Programming Language. ACM Trans. Program. Lang. Syst. Thibaut Balabonski, François Pottier, Jonathan Protzenko
2015	—	`conf`	A Few Lessons from the Mezzo Project. SNAPL François Pottier, Jonathan Protzenko
2015	B	`conf`	Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. ITP Arthur Charguéraud, François Pottier
2014	A	`conf`	Hindley-milner elaboration in applicative style: functional pearl. ICFP François Pottier
2014	Misc	`conf`	Type Soundness and Race Freedom for Mezzo. FLOPS Thibaut Balabonski, François Pottier, Jonathan Protzenko
2013	J	`jnl`	A step-indexed Kripke model of hidden state. Math. Struct. Comput. Sci. Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang
2013	J	`jnl`	Programming with Permissions in Mezzo. CoRR Jonathan Protzenko, François Pottier
2013	A	`conf`	Programming with permissions in Mezzo. ICFP François Pottier, Jonathan Protzenko
2013	J	`jnl`	Syntactic soundness proof of a type-and-capability system with hidden state. J. Funct. Program. François Pottier
2013	J	`jnl`	The ins and outs of iteration in Mezzo. CoRR Armaël Guéneau, François Pottier, Jonathan Protzenko
2012	J	`jnl`	A unified treatment of syntax with binders. J. Funct. Program. Nicolas Pouillard, François Pottier
2012	A	`conf`	Validating LR(1) Parsers. ESOP Jacques-Henri Jourdan, François Pottier, Xavier Leroy
2011	A*	`conf`	A typed store-passing translation for general references. POPL François Pottier
2011	—	`conf`	The essence of monotonic state. TLDI Alexandre Pilkiewicz, François Pottier
2010	B	`conf`	A Semantic Foundation for Hidden State. FoSSaCS Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus
2010	A	`conf`	A fresh look at programming with names and binders. ICFP Nicolas Pouillard, François Pottier
2008	B	`conf`	A Hoare Logic for Call-by-Value Functional Programs. MPC Yann Régis-Gianas, François Pottier
2008	A	`conf`	Functional translation of a calculus of capabilities. ICFP Arthur Charguéraud, François Pottier
2008	A*	`conf`	Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule. LICS François Pottier
2007	J	`jnl`	A constraint-based approach to guarded algebraic data types. ACM Trans. Program. Lang. Syst. Vincent Simonet, François Pottier
2007	—	`ed.`	Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007 TLDI François Pottier, George C. Necula
2007	A*	`conf`	Static Name Control for FreshML. LICS François Pottier
2006	J	`jnl`	Polymorphic typed defunctionalization and concretization. High. Order Symb. Comput. François Pottier, Nadji Gauthier
2006	—	`ed.`	Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006 ML Andrew Kennedy, François Pottier
2006	A*	`conf`	Stratified type inference for generalized algebraic data types. POPL François Pottier, Yann Régis-Gianas
2005	J	`jnl`	A systematic approach to static access control. ACM Trans. Program. Lang. Syst. François Pottier, Christian Skalka, Scott F. Smith
2005	—	`conf`	An Overview of C ML François Pottier
2005	A	`conf`	From ML type inference to stratified type inference. ICFP François Pottier
2005	—	`conf`	Subtyping Recursive Types Modulo Associative Commutative Products. TLCA Roberto Di Cosmo, François Pottier, Didier Rémy
2005	—	`conf`	Towards Efficient, Typed LR Parsers. ML François Pottier, Yann Régis-Gianas
2004	A	`conf`	Numbering matters: first-order canonical forms for second-order recursive types. ICFP Nadji Gauthier, François Pottier
2004	A*	`conf`	Polymorphic typed defunctionalization. POPL François Pottier, Nadji Gauthier
2003	J	`jnl`	Information flow inference for ML. ACM Trans. Program. Lang. Syst. François Pottier, Vincent Simonet
2003	J	`jnl`	Producing all ideals of a forest, functionally. J. Funct. Program. Jean-Christophe Filliâtre, François Pottier
2002	—	`conf`	A Simple View of Type-Secure Information Flow in the p-Calculus. CSFW François Pottier
2002	A*	`conf`	Information flow inference for ML. POPL François Pottier, Vincent Simonet
2002	—	`conf`	Syntactic Type Soundness for HM(X). TIP@MPC Christian Skalka, François Pottier
2001	A	`conf`	A Systematic Approach to Static Access Control. ESOP François Pottier, Christian Skalka, Scott F. Smith
2001	A	`conf`	JOIN(X): Constraint-Based Type Inference for the Join-Calculus. ESOP Sylvain Conchon, François Pottier
2001	J	`jnl`	Simplifying Subtyping Constraints: A Theory. Inf. Comput. François Pottier
2000	A	`conf`	A 3-Part Type Inference Engine. ESOP François Pottier
2000	J	`jnl`	A Versatile Constraint-Based Type Inference System. Nord. J. Comput. François Pottier
2000	A	`conf`	Information flow inference for free. ICFP François Pottier, Sylvain Conchon
1998	A	`conf`	A Framework for Type Inference with Subtyping. ICFP François Pottier
1996	A	`conf`	Simplifying Subtyping Constraints. ICFP François Pottier