François Pottier

According to our database, François Pottier authored at least 60 papers between 1996 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

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., January, 2024

2023

A High-Level Separation Logic for Heap Space under Garbage Collection.

Alexandre Moine, Arthur Charguéraud, François Pottier

Proc. ACM Program. Lang., January, 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 Type System for Effect Handlers and Dynamic Labels.

Paulo Emílio de Vilhena, François Pottier

Proceedings of the Programming Languages and Systems, 2023

2022

A separation logic for heap space under garbage collection.

Jean-Marie Madiot, François Pottier

Proc. ACM Program. Lang., 2022

Specification and verification of a transient stack.

Alexandre Moine, Arthur Charguéraud, François Pottier

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

A separation logic for effect handlers.

Paulo Emílio de Vilhena, François Pottier

Proc. ACM Program. Lang., 2021

Verifying a Minimalist Reverse-Mode AD Library.

Paulo Emílio de Vilhena, François Pottier

CoRR, 2021

Faster reachability analysis for LR(1) parsers.

Frédéric Bour, François Pottier

Proceedings of the SLE '21: 14th ACM SIGPLAN International Conference on Software Language Engineering, Chicago, IL, USA, October 17, 2021

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

Cosmo: a concurrent separation logic for multicore OCaml.

Glen Mével, Jacques-Henri Jourdan, François Pottier

Proc. ACM Program. Lang., 2020

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

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm.

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Time Credits and Time Receipts in Iris.

Glen Mével, Jacques-Henri Jourdan, François Pottier

Proceedings of the Programming Languages and Systems, 2019

2018

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification.

Armaël Guéneau, Arthur Charguéraud, François Pottier

Proceedings of the Programming Languages and Systems, 2018

2017

A Simple, Possibly Correct LR Parser for C11.

Jacques-Henri Jourdan, François Pottier

ACM Trans. Program. Lang. Syst., 2017

Visitors unchained.

François Pottier

Proc. ACM Program. Lang., 2017

Temporary Read-Only Permissions for Separation Logic.

Arthur Charguéraud, François Pottier

Proceedings of the Programming Languages and Systems, 2017

Verifying a hash table and its iterators in higher-order separation logic.

François Pottier

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

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

Reachability and error diagnosis in LR(1) parsers.

François Pottier

Proceedings of the 25th International Conference on Compiler Construction, 2016

2015

A Few Lessons from the Mezzo Project.

François Pottier, Jonathan Protzenko

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation.

Arthur Charguéraud, François Pottier

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

Hindley-milner elaboration in applicative style: functional pearl.

François Pottier

Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

Type Soundness and Race Freedom for Mezzo.

Thibaut Balabonski, François Pottier, Jonathan Protzenko

Proceedings of the Functional and Logic Programming - 12th International Symposium, 2014

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

Syntactic soundness proof of a type-and-capability system with hidden state.

François Pottier

J. Funct. Program., 2013

The ins and outs of iteration in Mezzo.

Armaël Guéneau, François Pottier, Jonathan Protzenko

CoRR, 2013

Programming with permissions in Mezzo.

François Pottier, Jonathan Protzenko

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

2012

A unified treatment of syntax with binders.

Nicolas Pouillard, François Pottier

J. Funct. Program., 2012

Validating LR(1) Parsers.

Jacques-Henri Jourdan, François Pottier, Xavier Leroy

Proceedings of the Programming Languages and Systems, 2012

2011

The essence of monotonic state.

Alexandre Pilkiewicz, François Pottier

Proceedings of TLDI 2011: 2011 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2011

A typed store-passing translation for general references.

François Pottier

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

2010

A fresh look at programming with names and binders.

Nicolas Pouillard, François Pottier

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

A Semantic Foundation for Hidden State.

Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus

Proceedings of the Foundations of Software Science and Computational Structures, 2010

2008

A Hoare Logic for Call-by-Value Functional Programs.

Yann Régis-Gianas, François Pottier

Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule.

François Pottier

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

Functional translation of a calculus of capabilities.

Arthur Charguéraud, François Pottier

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

2007

A constraint-based approach to guarded algebraic data types.

Vincent Simonet, François Pottier

ACM Trans. Program. Lang. Syst., 2007

Static Name Control for FreshML.

François Pottier

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2006

Polymorphic typed defunctionalization and concretization.

François Pottier, Nadji Gauthier

High. Order Symb. Comput., 2006

Stratified type inference for generalized algebraic data types.

François Pottier, Yann Régis-Gianas

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

2005

A systematic approach to static access control.

François Pottier, Christian Skalka, Scott F. Smith

ACM Trans. Program. Lang. Syst., 2005

Towards Efficient, Typed LR Parsers.

François Pottier, Yann Régis-Gianas

Proceedings of the ACM-SIGPLAN Workshop on ML, 2005

An Overview of C<i>alpha</i>ml.

François Pottier

Proceedings of the ACM-SIGPLAN Workshop on ML, 2005

Subtyping Recursive Types Modulo Associative Commutative Products.

Roberto Di Cosmo, François Pottier, Didier Rémy

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

From ML type inference to stratified type inference.

François Pottier

Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

2004

Polymorphic typed defunctionalization.

François Pottier, Nadji Gauthier

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

Numbering matters: first-order canonical forms for second-order recursive types.

Nadji Gauthier, François Pottier

Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, 2004

2003

Information flow inference for ML.

François Pottier, Vincent Simonet

ACM Trans. Program. Lang. Syst., 2003

Producing all ideals of a forest, functionally.

Jean-Christophe Filliâtre, François Pottier

J. Funct. Program., 2003

2002

Syntactic Type Soundness for HM(X).

Christian Skalka, François Pottier

Proceedings of the International Workshop in Types in Programming, 2002

A Simple View of Type-Secure Information Flow in the p-Calculus.

François Pottier

Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW-15 2002), 2002

2001

Simplifying Subtyping Constraints: A Theory.

François Pottier

Inf. Comput., 2001

JOIN(X): Constraint-Based Type Inference for the Join-Calculus.

Sylvain Conchon, François Pottier

Proceedings of the Programming Languages and Systems, 2001

2000

A Versatile Constraint-Based Type Inference System.

François Pottier

Nord. J. Comput., 2000

Information flow inference for free.

François Pottier, Sylvain Conchon

Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

A 3-Part Type Inference Engine.

François Pottier

Proceedings of the Programming Languages and Systems, 2000

1998

A Framework for Type Inference with Subtyping.

François Pottier

Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), 1998

1996

Simplifying Subtyping Constraints.

François Pottier

Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, 1996