Publications by François Pottier

[1] Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in Iris. Submitted, November 2018. [ bib | PDF ]
[2] 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 2018), volume 10801 of Lecture Notes in Computer Science, pages 533--560. Springer, April 2018. [ bib | PDF | Abstract ]
[3] François Pottier. Visitors unchained. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2017), September 2017. [ bib | DOI | PDF | Abstract ]
[4] 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, September 2017. [ bib | Software | PDF | At publisher's | Abstract ]
[5] 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. [ bib | Software | PDF | At publisher's ]
[6] François Pottier. Revisiting the CPS transformation and its implementation. Unpublished, July 2017. [ bib | PDF ]
[7] Arthur Charguéraud and François Pottier. Temporary read-only permissions for separation logic. In Hongseok Yang, editor, European Symposium on Programming (ESOP 2017), volume 10201 of Lecture Notes in Computer Science, pages 260--286. Springer, April 2017. [ bib | Software | PDF | Abstract ]
[8] 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 2017), pages 3--16, January 2017. [ bib | DOI | Software | PDF | At publisher's | Abstract ]
[9] 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. [ bib | DOI | Software | PDF | At publisher's | Abstract ]
[10] François Pottier. Reachability and error diagnosis in LR(1) parsers. In International Conference on Compiler Construction (CC 2016), pages 88--98, March 2016. [ bib | DOI | PDF | At publisher's | Abstract ]
[11] François Pottier. Reachability and error diagnosis in LR(1) automata. In Journées Francophones des Langages Applicatifs (JFLA 2016), January 2016. [ bib | PDF | At publisher's | Abstract ]
[12] 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 2015), volume 9236 of Lecture Notes in Computer Science, pages 137--153. Springer, August 2015. [ bib | Software | PDF | At publisher's | Abstract ]
[13] 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. [ bib | PDF | At publisher's | Abstract ]
[14] François Pottier. Depth-first search and strong connectivity in Coq. In Journées Francophones des Langages Applicatifs (JFLA 2015), January 2015. [ bib | Software | PDF | At publisher's | Abstract ]
[15] François Pottier. Hindley-Milner elaboration in applicative style. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2014), September 2014. [ bib | DOI | Software | PDF | At publisher's | Abstract ]
[16] Thibaut Balabonski, François Pottier, and Jonathan Protzenko. Type soundness and race freedom for Mezzo. In International Symposium on Functional and Logic Programming (FLOPS 2014), volume 8475 of Lecture Notes in Computer Science, pages 253--269. Springer, June 2014. [ bib | PDF | At publisher's | Abstract ]
[17] François Pottier and Jonathan Protzenko. Programming with permissions in Mezzo. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), pages 173--184, September 2013. [ bib | DOI | PDF | Long version | At publisher's | Abstract ]
[18] 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. [ bib | PDF | Abstract ]
[19] 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. [ bib | PDF | At publisher's ]
[20] 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. [ bib | PDF | At publisher's | Abstract ]
[21] Nicolas Pouillard and François Pottier. A unified treatment of syntax with binders. Journal of Functional Programming, 22(4--5):614--704, September 2012. [ bib | PDF | At publisher's | Abstract ]
[22] Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating LR(1) parsers. In European Symposium on Programming (ESOP 2012), volume 7211 of Lecture Notes in Computer Science, pages 397--416. Springer, March 2012. [ bib | PDF | At publisher's | Abstract ]
[23] François Pottier. A typed store-passing translation for general references. In ACM Symposium on Principles of Programming Languages (POPL 2011), Austin, Texas, January 2011. Supplementary material. [ bib | DOI | PDF | Long version | At publisher's | Abstract ]
[24] Alexandre Pilkiewicz and François Pottier. The essence of monotonic state. In ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2011), Austin, Texas, January 2011. [ bib | DOI | PDF | At publisher's | Abstract ]
[25] Nicolas Pouillard and François Pottier. A fresh look at programming with names and binders. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), pages 217--228, September 2010. [ bib | DOI | PDF | Long version | At publisher's | Abstract ]
[26] 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 2010), volume 6014 of Lecture Notes in Computer Science, pages 2--17. Springer, March 2010. [ bib | PDF | At publisher's | Abstract ]
[27] François Pottier. Lazy least fixed points in ML. Unpublished, December 2009. [ bib | PDF | Abstract ]
[28] François Pottier. Generalizing the higher-order frame and anti-frame rules. Unpublished, July 2009. [ bib | PDF | Abstract ]
[29] François Pottier. Three comments on the anti-frame rule. Unpublished, July 2009. [ bib | PDF | Abstract ]
[30] Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), pages 213--224, September 2008. [ bib | DOI | PDF | At publisher's | Abstract ]
[31] 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 2008), volume 5133 of Lecture Notes in Computer Science, pages 305--335. Springer, July 2008. [ bib | PDF | At publisher's | Abstract ]
[32] François Pottier. Hiding local state in direct style: a higher-order anti-frame rule. In Twenty-Third Annual IEEE Symposium on Logic In Computer Science (LICS 2008), pages 331--340, Pittsburgh, Pennsylvania, June 2008. [ bib | PDF | At publisher's | Abstract ]
[33] François Pottier. Static name control for FreshML. In Twenty-Second Annual IEEE Symposium on Logic In Computer Science (LICS 2007), pages 356--365, Wroclaw, Poland, July 2007. [ bib | PDF | Long version | At publisher's | Abstract ]
[34] 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. [ bib | DOI | PDF | At publisher's | Abstract ]
[35] François Pottier and Yann Régis-Gianas. Towards efficient, typed LR parsers. In ACM Workshop on ML, volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 155--180, March 2006. [ bib | PDF | At publisher's | Abstract ]
[36] François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation, 19:125--162, March 2006. [ bib | PDF | At publisher's | Abstract ]
[37] François Pottier. An overview of Cαml. In ACM Workshop on ML, volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 27--52, March 2006. [ bib | PDF | At publisher's | Abstract ]
[38] 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 2006), pages 232--244, Charleston, South Carolina, January 2006. [ bib | DOI | PDF | At publisher's | Abstract ]
[39] François Pottier and Yann Régis-Gianas. Menhir, December 2005. [ bib | Software ]
[40] François Pottier. A modern eye on ML type inference: old techniques and recent developments. Lecture notes for the APPSEM Summer School, September 2005. [ bib | PDF ]
[41] François Pottier. Cαml, June 2005. [ bib | Software ]
[42] 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. [ bib | PDF | Long version | At publisher's | Abstract ]
[43] 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. [ bib | DOI | PDF | At publisher's | Abstract ]
[44] Vincent Simonet and François Pottier. Constraint-based type inference for guarded algebraic data types. Research Report 5462, INRIA, January 2005. [ bib | PDF | At publisher's | Abstract ]
[45] 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. [ bib | PDF | At publisher's ]
[46] François Pottier. Types et contraintes. Mémoire d'habilitation à diriger des recherches, Université Paris 7, December 2004. [ bib | PDF ]
[47] 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 2004), pages 150--161, September 2004. [ bib | DOI | PDF | At publisher's | Abstract ]
[48] François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization. In ACM Symposium on Principles of Programming Languages (POPL 2004), pages 89--98, Venice, Italy, January 2004. Superseded by [36]. [ bib | DOI | PDF | At publisher's | Abstract ]
[49] 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. [ bib | PDF | At publisher's | Abstract ]
[50] François Pottier. A constraint-based presentation and generalization of rows. In Eighteenth Annual IEEE Symposium on Logic In Computer Science (LICS 2003), pages 331--340, Ottawa, Canada, June 2003. [ bib | PDF | Long version | At publisher's | Abstract ]
[51] François Pottier and Vincent Simonet. Information flow inference for ML. ACM Transactions on Programming Languages and Systems, 25(1):117--158, January 2003. [ bib | DOI | PDF | At publisher's | Abstract ]
[52] Christian Skalka and François Pottier. Syntactic type soundness for HM(X). In Workshop on Types in Programming (TIP 2002), volume 75 of Electronic Notes in Theoretical Computer Science, Dagstuhl, Germany, July 2002. [ bib | PDF | Abstract ]
[53] François Pottier. A simple view of type-secure information flow in the π-calculus. In IEEE Computer Security Foundations Workshop, pages 320--330, Cape Breton, Nova Scotia, June 2002. [ bib | PDF | Long version | At publisher's | Abstract ]
[54] François Pottier and Vincent Simonet. Information flow inference for ML. In ACM Symposium on Principles of Programming Languages (POPL 2002), pages 319--330, Portland, Oregon, January 2002. Superseded by [51]. [ bib | DOI | PDF | Long version | At publisher's | Abstract ]
[55] François Pottier. Simplifying subtyping constraints: a theory. Information & Computation, 170(2):153--183, November 2001. [ bib | PDF | At publisher's | Abstract ]
[56] François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. In David Sands, editor, European Symposium on Programming (ESOP 2001), volume 2028 of Lecture Notes in Computer Science, pages 30--45. Springer, April 2001. Superseded by [43]. [ bib | PDF | At publisher's | Abstract ]
[57] 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 2001), volume 2028 of Lecture Notes in Computer Science, pages 221--236. Springer, April 2001. [ bib | PDF | Long version | At publisher's | Abstract ]
[58] François Pottier. A semi-syntactic soundness proof for HM(X). Research Report 4150, INRIA, March 2001. [ bib | PDF | Abstract ]
[59] François Pottier. A versatile constraint-based type inference system. Nordic Journal of Computing, 7(4):312--347, November 2000. [ bib | PDF | Abstract ]
[60] François Pottier and Sylvain Conchon. Information flow inference for free. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), pages 46--57, Montréal, Canada, September 2000. [ bib | DOI | PDF | At publisher's | Abstract ]
[61] François Pottier. A 3-part type inference engine. In Gert Smolka, editor, European Symposium on Programming (ESOP 2000), volume 1782 of Lecture Notes in Computer Science, pages 320--335. Springer, March 2000. Superseded by [59]. [ bib | PDF | At publisher's | Abstract ]
[62] François Pottier. Wallace: an efficient implementation of type inference with subtyping, February 2000. [ bib | Software ]
[63] François Pottier. Type inference in the presence of subtyping: from theory to practice. Research Report 3483, INRIA, September 1998. [ bib | PDF | Abstract ]
[64] François Pottier. A framework for type inference with subtyping. In ACM SIGPLAN International Conference on Functional Programming (ICFP 1998), pages 228--238, September 1998. [ bib | DOI | PDF | At publisher's | Abstract ]
[65] 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. [ bib | PDF | Abstract ]
[66] François Pottier. Simplifying subtyping constraints. In ACM SIGPLAN International Conference on Functional Programming (ICFP 1996), pages 122--133, May 1996. [ bib | DOI | PDF | At publisher's | Abstract ]
[67] François Pottier. Type inference and simplification for recursively constrained types. In Actes du GDR Programmation 1995 (journée du pôle Programmation Fonctionnelle), November 1995. [ bib | PDF | Abstract ]
[68] François Pottier. Implémentation d'un système de modules évolué en Caml-Light. Research Report 2449, INRIA, January 1995. [ bib | PDF | At publisher's | Abstract ]
[69] Michel Mauny and François Pottier. An implementation of Caml Light with existential types. Technical Report 2183, INRIA, October 1993. [ bib | PDF | At publisher's | Abstract ]

This file was generated by bibtex2html 1.99.