Juliette Ponsonnet and François Pottier.
Verified persistent catenable deques.
Submitted, October 2025.
[ PDF ]
Verified persistent catenable deques.
Submitted, October 2025.
[ PDF ]
Frédéric Bour and François Pottier.
Mapping and explaining syntax errors with LRgrep.
Submitted, October 2025.
[ PDF ]
Mapping and explaining syntax errors with LRgrep.
Submitted, October 2025.
[ PDF ]
Remy Seassau, Irene Yoon, Jean-Marie Madiot, and François Pottier.
Formal semantics and program logics for a fragment of OCaml.
Proceedings of the ACM on Programming Languages, 9(ICFP), August 2025.
[ Software | PDF | At publisher's ]
Formal semantics and program logics for a fragment of OCaml.
Proceedings of the ACM on Programming Languages, 9(ICFP), August 2025.
[ Software | PDF | At publisher's ]
Jules Viennot, Arthur Wendling, Armaël Guéneau, and François Pottier.
Verified purely functional catenable real-time deques.
Submitted, May 2025.
[ PDF ]
Verified purely functional catenable real-time deques.
Submitted, May 2025.
[ PDF ]
Alexandre Moine, Arthur Charguéraud, and François Pottier.
Will it fit? verifying heap space bounds of concurrent programs under garbage collection with separation logic.
ACM Transactions on Programming Languages and Systems, 47(1), April 2025.
[ Software | PDF | At publisher's ]
Will it fit? verifying heap space bounds of concurrent programs under garbage collection with separation logic.
ACM Transactions on Programming Languages and Systems, 47(1), April 2025.
[ Software | PDF | At publisher's ]
Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan,
Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer.
Data race freedom à la mode.
Proceedings of the ACM on Programming Languages, 9(POPL):656--686, January 2025.
Distinguished Paper Award.
[ DOI | PDF ]
Data race freedom à la mode.
Proceedings of the ACM on Programming Languages, 9(POPL):656--686, January 2025.
Distinguished Paper Award.
[ DOI | PDF ]
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, and
Gabriel Scherer.
Tail modulo cons, OCaml, and relational separation logic.
Proceedings of the ACM on Programming Languages, 9(POPL):2337--2363, January 2025.
[ DOI | PDF | Long version ]
Tail modulo cons, OCaml, and relational separation logic.
Proceedings of the ACM on Programming Languages, 9(POPL):2337--2363, January 2025.
[ DOI | PDF | Long version ]
François Pottier.
Correct, fast LR(1) unparsing.
In Journées Francophones des Langages Applicatifs (JFLA), January 2024.
[ PDF | At publisher's ]
Correct, fast LR(1) unparsing.
In Journées Francophones des Langages Applicatifs (JFLA), January 2024.
[ PDF | At publisher's ]
François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, and Glen Mével.
Thunks and debits in separation logic with time credits.
Proceedings of the ACM on Programming Languages, 8(POPL), January 2024.
[ Software | PDF | At publisher's ]
Thunks and debits in separation logic with time credits.
Proceedings of the ACM on Programming Languages, 8(POPL), January 2024.
[ Software | PDF | At publisher's ]
Paulo Emílio de Vilhena and François Pottier.
Verifying an effect-handler-based define-by-run reverse-mode AD library.
Logical Methods in Computer Science, 19(4):5:1--5:51, October 2023.
[ PDF | At publisher's ]
Verifying an effect-handler-based define-by-run reverse-mode AD library.
Logical Methods in Computer Science, 19(4):5:1--5:51, October 2023.
[ PDF | At publisher's ]
Paulo Emílio de Vilhena and François Pottier.
A type system for effect handlers and dynamic labels.
In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer, April 2023.
[ PDF ]
A type system for effect handlers and dynamic labels.
In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer, April 2023.
[ PDF ]
Alexandre Moine, Arthur Charguéraud, and François Pottier.
A high-level separation logic for heap space under garbage collection.
Proceedings of the ACM on Programming Languages, 7(POPL), January 2023.
[ Software | PDF | At publisher's ]
A high-level separation logic for heap space under garbage collection.
Proceedings of the ACM on Programming Languages, 7(POPL), January 2023.
[ Software | PDF | At publisher's ]
Alexandre Moine, Arthur Charguéraud, and François Pottier.
Specification and verification of a transient stack.
In ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), January 2022.
Distinguished Paper Award.
[ Software | PDF | At publisher's ]
Specification and verification of a transient stack.
In ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), January 2022.
Distinguished Paper Award.
[ Software | PDF | At publisher's ]
Jean-Marie Madiot and François Pottier.
A separation logic for heap space under garbage collection.
Proceedings of the ACM on Programming Languages, 6(POPL):718--747, January 2022.
[ Software | PDF | At publisher's ]
A separation logic for heap space under garbage collection.
Proceedings of the ACM on Programming Languages, 6(POPL):718--747, January 2022.
[ Software | PDF | At publisher's ]
François Pottier.
Strong automated testing of OCaml libraries.
In Journées Francophones des Langages Applicatifs (JFLA), February 2021.
[ PDF ]
Strong automated testing of OCaml libraries.
In Journées Francophones des Langages Applicatifs (JFLA), February 2021.
[ PDF ]
Paulo Emílio de Vilhena and François Pottier.
A separation logic for effect handlers.
Proceedings of the ACM on Programming Languages, 5(POPL), January 2021.
[ Software | PDF | At publisher's ]
A separation logic for effect handlers.
Proceedings of the ACM on Programming Languages, 5(POPL), January 2021.
[ Software | PDF | At publisher's ]
Glen Mével, Jacques-Henri Jourdan, and François Pottier.
Cosmo: A concurrent separation logic for Multicore OCaml.
Proceedings of the ACM on Programming Languages, 4(ICFP), August 2020.
[ PDF | At publisher's ]
Cosmo: A concurrent separation logic for Multicore OCaml.
Proceedings of the ACM on Programming Languages, 4(ICFP), August 2020.
[ PDF | At publisher's ]
Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan.
Spy game: Verifying a local generic solver in Iris.
Proceedings of the ACM on Programming Languages, 4(POPL), January 2020.
[ PDF | At publisher's ]
Spy game: Verifying a local generic solver in Iris.
Proceedings of the ACM on Programming Languages, 4(POPL), January 2020.
[ PDF | At publisher's ]
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François
Pottier.
Formal proof and analysis of an incremental cycle detection algorithm.
In John Harrison, John O'Leary, and Andrew Tolmach, editors, Interactive Theorem Proving (ITP), volume 141 of Leibniz International Proceedings in Informatics, pages 18:1--18:20, Dagstuhl, Germany, September 2019. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[ PDF | At publisher's ]
Formal proof and analysis of an incremental cycle detection algorithm.
In John Harrison, John O'Leary, and Andrew Tolmach, editors, Interactive Theorem Proving (ITP), volume 141 of Leibniz International Proceedings in Informatics, pages 18:1--18:20, Dagstuhl, Germany, September 2019. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[ PDF | At publisher's ]
Glen Mével, Jacques-Henri Jourdan, and François Pottier.
Time credits and time receipts in Iris.
In Luis Caires, editor, European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 1--27. Springer, April 2019.
[ PDF | At publisher's ]
Time credits and time receipts in Iris.
In Luis Caires, editor, European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 1--27. Springer, April 2019.
[ PDF | At publisher's ]
Arthur Charguéraud and François Pottier.
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits.
Journal of Automated Reasoning, 62(3):331--365, March 2019.
[ Software | PDF | At publisher's ]
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits.
Journal of Automated Reasoning, 62(3):331--365, March 2019.
[ Software | PDF | At publisher's ]
Armaël Guéneau, Arthur Charguéraud, and François Pottier.
A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification.
In Amal Ahmed, editor, European Symposium on Programming (ESOP), volume 10801 of Lecture Notes in Computer Science, pages 533--560. Springer, April 2018.
[ PDF | At publisher's ]
A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification.
In Amal Ahmed, editor, European Symposium on Programming (ESOP), volume 10801 of Lecture Notes in Computer Science, pages 533--560. Springer, April 2018.
[ PDF | At publisher's ]
François Pottier.
Visitors unchained.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2017.
[ PDF | At publisher's ]
Visitors unchained.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2017.
[ PDF | At publisher's ]
Jacques-Henri Jourdan and François Pottier.
A simple, possibly correct LR parser for C11.
ACM Transactions on Programming Languages and Systems, 39(4):14:1--14:36, August 2017.
[ Software | PDF | At publisher's ]
A simple, possibly correct LR parser for C11.
ACM Transactions on Programming Languages and Systems, 39(4):14:1--14:36, August 2017.
[ Software | PDF | At publisher's ]
François Pottier.
Revisiting the CPS transformation and its implementation.
Unpublished, July 2017.
[ PDF ]
Revisiting the CPS transformation and its implementation.
Unpublished, July 2017.
[ PDF ]
François Pottier.
Verifying a hash table and its iterators in higher-order separation logic.
In ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), pages 3--16, January 2017.
[ DOI | Software | PDF | At publisher's ]
Verifying a hash table and its iterators in higher-order separation logic.
In ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), pages 3--16, January 2017.
[ DOI | Software | PDF | At publisher's ]
Thibaut Balabonski, François Pottier, and Jonathan Protzenko.
The design and formalization of Mezzo, a permission-based programming language.
ACM Transactions on Programming Languages and Systems, 38(4):14:1--14:94, August 2016.
[ DOI | Software | PDF | At publisher's ]
The design and formalization of Mezzo, a permission-based programming language.
ACM Transactions on Programming Languages and Systems, 38(4):14:1--14:94, August 2016.
[ DOI | Software | PDF | At publisher's ]
François Pottier.
Reachability and error diagnosis in LR(1) parsers.
In International Conference on Compiler Construction (CC), pages 88--98, March 2016.
[ DOI | PDF | At publisher's ]
Reachability and error diagnosis in LR(1) parsers.
In International Conference on Compiler Construction (CC), pages 88--98, March 2016.
[ DOI | PDF | At publisher's ]
François Pottier.
Reachability and error diagnosis in LR(1) automata.
In Journées Francophones des Langages Applicatifs (JFLA), January 2016.
[ PDF | At publisher's ]
Reachability and error diagnosis in LR(1) automata.
In Journées Francophones des Langages Applicatifs (JFLA), January 2016.
[ PDF | At publisher's ]
Arthur Charguéraud and François Pottier.
Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation.
In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 137--153. Springer, August 2015.
[ Software | PDF | At publisher's ]
Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation.
In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 137--153. Springer, August 2015.
[ Software | PDF | At publisher's ]
François Pottier and Jonathan Protzenko.
A few lessons from the Mezzo project.
In Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett, editors, Summit oN Advances in Programming Languages (SNAPL), volume 32 of Leibniz International Proceedings in Informatics, pages 221--237. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, May 2015.
[ PDF | At publisher's ]
A few lessons from the Mezzo project.
In Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett, editors, Summit oN Advances in Programming Languages (SNAPL), volume 32 of Leibniz International Proceedings in Informatics, pages 221--237. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, May 2015.
[ PDF | At publisher's ]
François Pottier.
Depth-first search and strong connectivity in Coq.
In Journées Francophones des Langages Applicatifs (JFLA), January 2015.
[ Software | PDF | At publisher's ]
Depth-first search and strong connectivity in Coq.
In Journées Francophones des Langages Applicatifs (JFLA), January 2015.
[ Software | PDF | At publisher's ]
François Pottier.
Hindley-Milner elaboration in applicative style.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2014.
[ DOI | Software | PDF | At publisher's ]
Hindley-Milner elaboration in applicative style.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2014.
[ DOI | Software | PDF | At publisher's ]
Thibaut Balabonski, François Pottier, and Jonathan Protzenko.
Type soundness and race freedom for Mezzo.
In International Symposium on Functional and Logic Programming (FLOPS), volume 8475 of Lecture Notes in Computer Science, pages 253--269. Springer, June 2014.
[ PDF | At publisher's ]
Type soundness and race freedom for Mezzo.
In International Symposium on Functional and Logic Programming (FLOPS), volume 8475 of Lecture Notes in Computer Science, pages 253--269. Springer, June 2014.
[ PDF | At publisher's ]
François Pottier and Jonathan Protzenko.
Programming with permissions in Mezzo.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 173--184, September 2013.
[ DOI | PDF | Long version | At publisher's ]
Programming with permissions in Mezzo.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 173--184, September 2013.
[ DOI | PDF | Long version | At publisher's ]
Armaël Guéneau, François Pottier, and Jonathan Protzenko.
The ins and outs of iteration in Mezzo.
Talk proposal for HOPE 2013, July 2013.
[ PDF ]
The ins and outs of iteration in Mezzo.
Talk proposal for HOPE 2013, July 2013.
[ PDF ]
Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian
Støvring, and Hongseok Yang.
A step-indexed Kripke model of hidden state.
Mathematical Structures in Computer Science, 23(1):1--54, February 2013.
[ PDF | At publisher's ]
A step-indexed Kripke model of hidden state.
Mathematical Structures in Computer Science, 23(1):1--54, February 2013.
[ PDF | At publisher's ]
François Pottier.
Syntactic soundness proof of a type-and-capability system with hidden state.
Journal of Functional Programming, 23(1):38--144, January 2013.
[ PDF | At publisher's ]
Syntactic soundness proof of a type-and-capability system with hidden state.
Journal of Functional Programming, 23(1):38--144, January 2013.
[ PDF | At publisher's ]
Nicolas Pouillard and François Pottier.
A unified treatment of syntax with binders.
Journal of Functional Programming, 22(4--5):614--704, September 2012.
[ PDF | At publisher's ]
A unified treatment of syntax with binders.
Journal of Functional Programming, 22(4--5):614--704, September 2012.
[ PDF | At publisher's ]
Jacques-Henri Jourdan, François Pottier, and Xavier Leroy.
Validating LR(1) parsers.
In European Symposium on Programming (ESOP), volume 7211 of Lecture Notes in Computer Science, pages 397--416. Springer, March 2012.
[ PDF | At publisher's ]
Validating LR(1) parsers.
In European Symposium on Programming (ESOP), volume 7211 of Lecture Notes in Computer Science, pages 397--416. Springer, March 2012.
[ PDF | At publisher's ]
François Pottier.
A typed store-passing translation for general references.
In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, January 2011.
Supplementary material.
[ DOI | PDF | Long version | At publisher's ]
A typed store-passing translation for general references.
In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, January 2011.
Supplementary material.
[ DOI | PDF | Long version | At publisher's ]
Alexandre Pilkiewicz and François Pottier.
The essence of monotonic state.
In ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), Austin, Texas, January 2011.
[ DOI | PDF | At publisher's ]
The essence of monotonic state.
In ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), Austin, Texas, January 2011.
[ DOI | PDF | At publisher's ]
Nicolas Pouillard and François Pottier.
A fresh look at programming with names and binders.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 217--228, September 2010.
[ DOI | PDF | Long version | At publisher's ]
A fresh look at programming with names and binders.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 217--228, September 2010.
[ DOI | PDF | Long version | At publisher's ]
Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, and
Bernhard Reus.
A semantic foundation for hidden state.
In C.-H. L. Ong, editor, International Conference on Foundations of Software Science and Computational Structures (FOSSACS), volume 6014 of Lecture Notes in Computer Science, pages 2--17. Springer, March 2010.
[ PDF | At publisher's ]
A semantic foundation for hidden state.
In C.-H. L. Ong, editor, International Conference on Foundations of Software Science and Computational Structures (FOSSACS), volume 6014 of Lecture Notes in Computer Science, pages 2--17. Springer, March 2010.
[ PDF | At publisher's ]
François Pottier.
Generalizing the higher-order frame and anti-frame rules.
Unpublished, July 2009.
[ PDF ]
Generalizing the higher-order frame and anti-frame rules.
Unpublished, July 2009.
[ PDF ]
Arthur Charguéraud and François Pottier.
Functional translation of a calculus of capabilities.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 213--224, September 2008.
[ DOI | PDF | At publisher's ]
Functional translation of a calculus of capabilities.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 213--224, September 2008.
[ DOI | PDF | At publisher's ]
Yann Régis-Gianas and François Pottier.
A Hoare logic for call-by-value functional programs.
In International Conference on Mathematics of Program Construction (MPC), volume 5133 of Lecture Notes in Computer Science, pages 305--335. Springer, July 2008.
[ PDF | At publisher's ]
A Hoare logic for call-by-value functional programs.
In International Conference on Mathematics of Program Construction (MPC), volume 5133 of Lecture Notes in Computer Science, pages 305--335. Springer, July 2008.
[ PDF | At publisher's ]
François Pottier.
Hiding local state in direct style: a higher-order anti-frame rule.
In IEEE Symposium on Logic In Computer Science (LICS), pages 331--340, Pittsburgh, Pennsylvania, June 2008.
[ PDF | At publisher's ]
Hiding local state in direct style: a higher-order anti-frame rule.
In IEEE Symposium on Logic In Computer Science (LICS), pages 331--340, Pittsburgh, Pennsylvania, June 2008.
[ PDF | At publisher's ]
François Pottier.
Static name control for FreshML.
In IEEE Symposium on Logic In Computer Science (LICS), pages 356--365, Wroclaw, Poland, July 2007.
[ PDF | Long version | At publisher's ]
Static name control for FreshML.
In IEEE Symposium on Logic In Computer Science (LICS), pages 356--365, Wroclaw, Poland, July 2007.
[ PDF | Long version | At publisher's ]
Vincent Simonet and François Pottier.
A constraint-based approach to guarded algebraic data types.
ACM Transactions on Programming Languages and Systems, 29(1), January 2007.
[ DOI | PDF | At publisher's ]
A constraint-based approach to guarded algebraic data types.
ACM Transactions on Programming Languages and Systems, 29(1), January 2007.
[ DOI | PDF | At publisher's ]
François Pottier and Yann Régis-Gianas.
Towards efficient, typed LR parsers.
In ACM Workshop on ML (ML), volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 155--180, March 2006.
[ PDF | At publisher's ]
Towards efficient, typed LR parsers.
In ACM Workshop on ML (ML), volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 155--180, March 2006.
[ PDF | At publisher's ]
François Pottier and Nadji Gauthier.
Polymorphic typed defunctionalization and concretization.
Higher-Order and Symbolic Computation, 19:125--162, March 2006.
[ PDF | At publisher's ]
Polymorphic typed defunctionalization and concretization.
Higher-Order and Symbolic Computation, 19:125--162, March 2006.
[ PDF | At publisher's ]
François Pottier.
An overview of Cαml.
In ACM Workshop on ML (ML), volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 27--52, March 2006.
[ PDF | At publisher's ]
An overview of Cαml.
In ACM Workshop on ML (ML), volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 27--52, March 2006.
[ PDF | At publisher's ]
François Pottier and Yann Régis-Gianas.
Stratified type inference for generalized algebraic data types.
In ACM Symposium on Principles of Programming Languages (POPL), pages 232--244, Charleston, South Carolina, January 2006.
[ DOI | PDF | At publisher's ]
Stratified type inference for generalized algebraic data types.
In ACM Symposium on Principles of Programming Languages (POPL), pages 232--244, Charleston, South Carolina, January 2006.
[ DOI | PDF | At publisher's ]
François Pottier.
A modern eye on ML type inference: old techniques and recent developments.
Lecture notes for the APPSEM Summer School, September 2005.
[ PDF ]
A modern eye on ML type inference: old techniques and recent developments.
Lecture notes for the APPSEM Summer School, September 2005.
[ PDF ]
Roberto Di Cosmo, François Pottier, and Didier Rémy.
Subtyping recursive types modulo associative commutative products.
In Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), volume 3461 of Lecture Notes in Computer Science, pages 179--193, Nara, Japan, April 2005. Springer.
[ PDF | Long version | At publisher's ]
Subtyping recursive types modulo associative commutative products.
In Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), volume 3461 of Lecture Notes in Computer Science, pages 179--193, Nara, Japan, April 2005. Springer.
[ PDF | Long version | At publisher's ]
François Pottier, Christian Skalka, and Scott Smith.
A systematic approach to static access control.
ACM Transactions on Programming Languages and Systems, 27(2):344--382, March 2005.
[ DOI | PDF | At publisher's ]
A systematic approach to static access control.
ACM Transactions on Programming Languages and Systems, 27(2):344--382, March 2005.
[ DOI | PDF | At publisher's ]
Vincent Simonet and François Pottier.
Constraint-based type inference for guarded algebraic data types.
Research Report 5462, INRIA, January 2005.
[ PDF | At publisher's ]
Constraint-based type inference for guarded algebraic data types.
Research Report 5462, INRIA, January 2005.
[ PDF | At publisher's ]
François Pottier and Didier Rémy.
The essence of ML type inference.
In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005.
A draft extended version is also available.
[ PDF | At publisher's ]
The essence of ML type inference.
In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005.
A draft extended version is also available.
[ PDF | At publisher's ]
François Pottier.
Types et contraintes.
Mémoire d'habilitation à diriger des recherches, Université Paris 7, December 2004.
[ PDF ]
Types et contraintes.
Mémoire d'habilitation à diriger des recherches, Université Paris 7, December 2004.
[ PDF ]
Nadji Gauthier and François Pottier.
Numbering matters: First-order canonical forms for second-order recursive types.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 150--161, September 2004.
[ DOI | PDF | At publisher's ]
Numbering matters: First-order canonical forms for second-order recursive types.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 150--161, September 2004.
[ DOI | PDF | At publisher's ]
François Pottier and Nadji Gauthier.
Polymorphic typed defunctionalization.
In ACM Symposium on Principles of Programming Languages (POPL), pages 89--98, Venice, Italy, January 2004.
Superseded by [57].
[ DOI | PDF | At publisher's ]
Polymorphic typed defunctionalization.
In ACM Symposium on Principles of Programming Languages (POPL), pages 89--98, Venice, Italy, January 2004.
Superseded by [57].
[ DOI | PDF | At publisher's ]
Jean-Christophe Filliâtre and François Pottier.
Producing all ideals of a forest, functionally.
Journal of Functional Programming, 13(5):945--956, September 2003.
[ PDF | At publisher's ]
Producing all ideals of a forest, functionally.
Journal of Functional Programming, 13(5):945--956, September 2003.
[ PDF | At publisher's ]
François Pottier.
A constraint-based presentation and generalization of rows.
In IEEE Symposium on Logic In Computer Science (LICS), pages 331--340, Ottawa, Canada, June 2003.
[ PDF | Long version | At publisher's ]
A constraint-based presentation and generalization of rows.
In IEEE Symposium on Logic In Computer Science (LICS), pages 331--340, Ottawa, Canada, June 2003.
[ PDF | Long version | At publisher's ]
François Pottier and Vincent Simonet.
Information flow inference for ML.
ACM Transactions on Programming Languages and Systems, 25(1):117--158, January 2003.
[ DOI | PDF | At publisher's ]
Information flow inference for ML.
ACM Transactions on Programming Languages and Systems, 25(1):117--158, January 2003.
[ DOI | PDF | At publisher's ]
Christian Skalka and François Pottier.
Syntactic type soundness for HM(X).
In Workshop on Types in Programming (TIP), volume 75 of Electronic Notes in Theoretical Computer Science, Dagstuhl, Germany, July 2002.
[ PDF ]
Syntactic type soundness for HM(X).
In Workshop on Types in Programming (TIP), volume 75 of Electronic Notes in Theoretical Computer Science, Dagstuhl, Germany, July 2002.
[ PDF ]
François Pottier.
A simple view of type-secure information flow in the π-calculus.
In IEEE Computer Security Foundations Workshop (CSFW), pages 320--330, Cape Breton, Nova Scotia, June 2002.
[ PDF | Long version | At publisher's ]
A simple view of type-secure information flow in the π-calculus.
In IEEE Computer Security Foundations Workshop (CSFW), pages 320--330, Cape Breton, Nova Scotia, June 2002.
[ PDF | Long version | At publisher's ]
François Pottier and Vincent Simonet.
Information flow inference for ML.
In ACM Symposium on Principles of Programming Languages (POPL), pages 319--330, Portland, Oregon, January 2002.
Superseded by [70].
[ DOI | PDF | Long version | At publisher's ]
Information flow inference for ML.
In ACM Symposium on Principles of Programming Languages (POPL), pages 319--330, Portland, Oregon, January 2002.
Superseded by [70].
[ DOI | PDF | Long version | At publisher's ]
François Pottier.
Simplifying subtyping constraints: a theory.
Information & Computation, 170(2):153--183, November 2001.
[ PDF | At publisher's ]
Simplifying subtyping constraints: a theory.
Information & Computation, 170(2):153--183, November 2001.
[ PDF | At publisher's ]
François Pottier, Christian Skalka, and Scott Smith.
A systematic approach to static access control.
In David Sands, editor, European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 30--45. Springer, April 2001.
Superseded by [62].
[ PDF | At publisher's ]
A systematic approach to static access control.
In David Sands, editor, European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 30--45. Springer, April 2001.
Superseded by [62].
[ PDF | At publisher's ]
Sylvain Conchon and François Pottier.
JOIN(X): Constraint-based type inference for the join-calculus.
In David Sands, editor, European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 221--236. Springer, April 2001.
[ PDF | Long version | At publisher's ]
JOIN(X): Constraint-based type inference for the join-calculus.
In David Sands, editor, European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 221--236. Springer, April 2001.
[ PDF | Long version | At publisher's ]
François Pottier.
A semi-syntactic soundness proof for HM(X).
Research Report 4150, INRIA, March 2001.
[ PDF ]
A semi-syntactic soundness proof for HM(X).
Research Report 4150, INRIA, March 2001.
[ PDF ]
François Pottier.
A versatile constraint-based type inference system.
Nordic Journal of Computing, 7(4):312--347, November 2000.
[ PDF ]
A versatile constraint-based type inference system.
Nordic Journal of Computing, 7(4):312--347, November 2000.
[ PDF ]
François Pottier and Sylvain Conchon.
Information flow inference for free.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 46--57, Montréal, Canada, September 2000.
[ DOI | PDF | At publisher's ]
Information flow inference for free.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 46--57, Montréal, Canada, September 2000.
[ DOI | PDF | At publisher's ]
François Pottier.
A 3-part type inference engine.
In Gert Smolka, editor, European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 320--335. Springer, March 2000.
Superseded by [78].
[ PDF | At publisher's ]
A 3-part type inference engine.
In Gert Smolka, editor, European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 320--335. Springer, March 2000.
Superseded by [78].
[ PDF | At publisher's ]
François Pottier.
Type inference in the presence of subtyping: from theory to practice.
Research Report 3483, INRIA, September 1998.
[ PDF ]
Type inference in the presence of subtyping: from theory to practice.
Research Report 3483, INRIA, September 1998.
[ PDF ]
François Pottier.
A framework for type inference with subtyping.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 228--238, September 1998.
[ DOI | PDF | At publisher's ]
A framework for type inference with subtyping.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 228--238, September 1998.
[ DOI | PDF | At publisher's ]
François Pottier.
Synthèse de types en présence de sous-typage: de la théorie à la pratique.
PhD thesis, Université Paris 7, July 1998.
[ PDF ]
Synthèse de types en présence de sous-typage: de la théorie à la pratique.
PhD thesis, Université Paris 7, July 1998.
[ PDF ]
François Pottier.
Simplifying subtyping constraints.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 122--133, May 1996.
[ DOI | PDF | At publisher's ]
Simplifying subtyping constraints.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 122--133, May 1996.
[ DOI | PDF | At publisher's ]
François Pottier.
Type inference and simplification for recursively constrained types.
In Actes du GDR Programmation (journée du pôle Programmation Fonctionnelle), November 1995.
[ PDF ]
Type inference and simplification for recursively constrained types.
In Actes du GDR Programmation (journée du pôle Programmation Fonctionnelle), November 1995.
[ PDF ]
François Pottier.
Implémentation d'un système de modules évolué en Caml-Light.
Research Report 2449, INRIA, January 1995.
[ PDF | At publisher's ]
Implémentation d'un système de modules évolué en Caml-Light.
Research Report 2449, INRIA, January 1995.
[ PDF | At publisher's ]
Michel Mauny and François Pottier.
An implementation of Caml Light with existential types.
Technical Report 2183, INRIA, October 1993.
[ PDF | At publisher's ]
An implementation of Caml Light with existential types.
Technical Report 2183, INRIA, October 1993.
[ PDF | At publisher's ]