Talks by François Pottier and co-authors

François Pottier.
A separation logic for heap space under garbage collection, January 2022.
Talk given at POPL 2022 (online).
PDF ]
François Pottier.
A separation logic for heap space under garbage collection, December 2021.
Talk given at Inria, Paris, France.
PDF ]
François Pottier.
Strong automated testing of OCaml libraries, June 2021.
Talk given at IFIP WG 2.16 (online) and at Inria Paris and at Nomadic Labs, Paris.
PDF ]
François Pottier.
Raisonner à propos du temps en logique de séparation, April 2021.
Talk given at Collège de France, Paris, France. In French.
PDF ]
Glen Mével.
Cosmo: A concurrent separation logic for Multicore OCaml, August 2020.
Talk given at ICFP 2020.
Video | PDF ]
Paulo Emílio de Vilhena.
Spy game: Verifying a local generic solver in Iris, January 2020.
Talk given at POPL 2020, New Orleans.
Video | PDF ]
François Pottier.
Playing spy games in Iris, November 2019.
Talk given at IFIP WG 2.16, Nice, France.
PDF ]
François Pottier.
Cambium en 180 secondes, November 2019.
3-minute presentation given at Inria, Paris, France.
PDF ]
François Pottier.
Playing spy games in Iris, October 2019.
Talk given at the Iris Workshop, Aarhus, Denmark.
PDF ]
Glen Mével.
Time credits and time receipts in Iris, April 2019.
Talk given at ESOP 2019, Prague, Czech Republic.
PDF ]
Armaël Guéneau.
Formalizing asymptotic complexity claims via deductive program verification, April 2018.
Talk given at ESOP 2018, Thessaloniki, Greece.
PDF ]
François Pottier.
Mezzo: an experience report, December 2017.
Talk given at ENS, Lyon, France.
PDF ]
François Pottier.
Visitors unchained, September 2017.
Talk given at ICFP 2017, Oxford, United Kingdom.
PDF ]
François Pottier.
Visitors unchained, June 2017.
Talk given at IFIP WG 2.8, Edinburgh, Scotland.
PDF ]
François Pottier.
Visitors unchained, May 2017.
Talk given at Inria, Paris, France.
PDF ]
François Pottier.
Temporary read-only permissions for separation logic, April 2017.
Talk given at Inria, Paris, France.
PDF ]
François Pottier.
Temporary read-only permissions for separation logic, April 2017.
Talk given by Armaël Guéneau at ESOP 2017, Uppsala, Sweden.
PDF ]
François Pottier.
Verifying a hash table and its iterators in higher-order separation logic, January 2017.
Talk given at CPP 2017, Paris, France.
PDF ]
François Pottier.
Temporary read-only permissions for separation logic, November 2016.
Talk given in Saclay, France.
PDF ]
François Pottier.
Mezzo: an experience report, October 2016.
Talk given at IFIP WG 2.16, Lausanne, Switzerland.
PDF ]
François Pottier.
Reachability and error diagnosis in LR(1) parsers, March 2016.
Talk given at CC 2016, Barcelona, Spain.
PDF ]
François Pottier.
Reachability and error diagnosis in LR(1) automata, January 2016.
Talk given at JFLA 2016, Saint-Malo, France.
PDF ]
François Pottier.
Explaining syntax errors (LR de rien, c'est pas facile), November 2015.
Talk given at the OCaml Users meeting, Paris, France.
PDF ]
Arthur Charguéraud and François Pottier.
Machine-checked correctness and complexity of a union-find implementation, September 2015.
Talk given at Microsoft Research, Redmond, Washington.
Video | PDF ]
François Pottier.
Type inference, August 2015.
Talk given at PLMW @ ICFP 2015, Vancouver, Canada.
PDF ]
François Pottier.
An overview of Mezzo, June 2015.
Lecture given at SFM-15:MP, Bertinoro, Italy. See also the accompanying code.
PDF ]
François Pottier.
Depth-first search and strong connectivity in Coq, January 2015.
Talk given at JFLA 2015, le Val d'Ajol, France.
PDF ]
François Pottier.
Hindley-Milner elaboration in applicative style, September 2014.
Talk given at ICFP 2014, Göteborg, Sweden.
PDF ]
François Pottier.
Type soundness and data race freedom for Mezzo, June 2014.
Talk given at FLOPS 2014, Kanazawa, Japan.
PDF ]
François Pottier.
The theory of Mezzo, April 2014.
Lecture given at Institut Henri Poincaré, Paris, France.
Video | PDF ]
François Pottier.
The practice of Mezzo, April 2014.
Lecture given at Institut Henri Poincaré, Paris, France. See also the accompanying code.
Video | PDF ]
François Pottier.
The design of Mezzo, September 2013.
Talk given at Carnegie Mellon University, Pittsburgh, USA; at IFIP WG 2.8, Aussois, France; and at Aarhus University, Denmark.
PDF ]
François Pottier.
A bird's eye view of Mezzo, November 2012.
Talk given at Microsoft Research, Cambridge, UK.
PDF ]
François Pottier.
Types for complexity-checking, March 2011.
Talk given at ENS, Lyon, France.
PDF ]
François Pottier.
A type-preserving store-passing translation for general references, January 2011.
Talk given at POPL 2011, Austin, Texas.
PDF ]
François Pottier.
Types for complexity-checking, January 2011.
Talk given at JFLA 2011, La Bresse, France.
PDF ]
François Pottier.
Types for complexity-checking, May 2010.
Talk given at ENS, Lyon, France.
PDF ]
François Pottier.
Hidden state and the anti-frame rule, December 2009.
Talk given at Université Paris 7, Paris, France.
PDF ]
François Pottier.
A type-preserving store-passing translation for general references, November 2009.
Talk given at Université Paris 7, Paris, France.
PDF ]
François Pottier.
Gala de GAFs à gogo, March 2009.
Talk given at Verimag, Grenoble, France.
PDF ]
Arthur Charguéraud.
Functional translation of a calculus of capabilities, September 2008.
Talk given at ICFP 2008, Victoria, Canada.
PDF ]
François Pottier.
Hiding local state in direct style, September 2008.
Talk given at Université Paris 7, Paris, France.
PDF ]
Yann Régis-Gianas.
A Hoare logic for call-by-value functional programs, July 2008.
Talk given at MPC 2008, Marseille, France.
PDF ]
François Pottier.
Hiding local state in direct style: a higher-order anti-frame rule, June 2008.
Talk given at IFIP WG 2.8, Park City, Utah.
PDF ]
François Pottier.
Hiding local state in direct style, June 2008.
Talk given at LICS 2008, Pittsburgh, Pennsylvania.
PDF ]
François Pottier.
Hiding local state in direct style: a higher-order anti-frame rule, February 2008.
Talk given in Schloss Dagstuhl, Germany.
PDF ]
François Pottier.
Hiding local state in direct style: a higher-order anti-frame rule, January 2008.
Talk given at INRIA, Rocquencourt.
PDF ]
François Pottier.
Static name control for FreshML, July 2007.
Talk given at LICS 2007, Wroclaw, Poland.
PDF ]
François Pottier.
Wandering through linear types, capabilities, and regions, May 2007.
Survey talk given at INRIA, Rocquencourt, France.
PDF ]
François Pottier.
Static name control for FreshML, May 2007.
Talk given in Edinburgh, Great Britain.
PDF ]
François Pottier.
Static name control for FreshML, September 2006.
Talk given at Cambridge University, Great Britain.
PDF ]
François Pottier.
Un aperçu de Menhir, March 2006.
Talk given at Université Paris 7, France.
PDF ]
Yann Régis-Gianas.
Stratified type inference for generalized algebraic data types, January 2006.
Talk given at POPL 2006, Charleston, South Carolina.
PDF ]
François Pottier.
Un aperçu de Menhir, January 2006.
Talk given at INRIA, Rocquencourt, France.
PDF ]
François Pottier.
An overview of Cαml, September 2005.
Talk given at the ML Workshop, Tallinn, Estonia.
PDF ]
François Pottier.
Where is ML type inference headed? Constraint solving meets local shape inference, September 2005.
Invited talk given at ICFP 2005, Tallinn, Estonia.
PDF ]
François Pottier.
A modern eye on ML type inference: old techniques and recent developments, September 2005.
Course given at the APPSEM Summer School, Frauenchiemsee, Germany.
PDF ]
François Pottier.
Présentation de Cαml, July 2005.
Talk given at LRI, Orsay, France.
PDF ]
François Pottier.
Towards efficient, typed LR parsers, June 2005.
Talk given in Schloss Dagstuhl, Germany.
PDF ]
François Pottier.
Vers des analyseurs syntaxiques efficaces et bien typés, January 2005.
Talk given at ENS, Lyon, France.
PDF ]
François Pottier.
Type-based information flow analyses, January 2005.
Course given at the CIMPA School on Security of Computer Systems and Networks, Bangalore, India.
PDF ]
François Pottier.
Types et contraintes, December 2004.
Soutenance d'habilitation à diriger des recherches, Université Paris 7.
PDF ]
François Pottier.
Constraint-based type inference for GADTs, November 2004.
Talk given at Microsoft Research, Cambridge, UK.
PDF ]
Nadji Gauthier.
Numbering matters: First-order canonical forms for second-order recursive types, September 2004.
Talk given at ICFP 2004, Snowbird, Utah. Animations in the slides require the advi viewer.
DVI ]
François Pottier.
Type-based information flow analyses, June 2004.
Course given at the Summer School on Software Security, Eugene, Oregon.
PDF ]
François Pottier.
Polymorphic typed defunctionalization, January 2004.
Talk given at POPL 2004, Venice, Italy.
PDF | DVI | PostScript ]
François Pottier.
A constraint-based presentation and generalization of rows, June 2003.
Talk given at LICS 2003, Ottawa, Canada.
PostScript ]
François Pottier.
A constraint-based presentation of rows, December 2002.
Talk given at ENS, Paris, France.
PostScript ]
François Pottier.
A simple view of type-secure information flow in the π-calculus, June 2002.
Talk given at CSFW'15, Cape Breton, Canada.
PDF | PostScript ]
François Pottier.
Sécurité par le typage, May 2002.
Short presentation given at INRIA, Rocquencourt, France.
PostScript ]
François Pottier.
Proving the correctness of type-based information flow analyses: some approaches, April 2002.
Talk given at the Profundis meeting, INRIA, Sophia, France.
PostScript ]
François Pottier.
Une présentation moderne de l'inférence de types pour ML, March 2002.
Talk given at INRIA, Rocquencourt, France.
DVI ]
François Pottier.
Types for information flow analysis, March 2002.
Course given at the Spring School on Semantics of Programming Languages, Agay, France.
PostScript ]
Vincent Simonet.
Information flow inference for ML, January 2002.
Talk given at POPL 2002, Portland, Oregon.
PDF ]
François Pottier.
Inférence de types à base de contraintes, November 2001.
Talk given at IRIT, Toulouse, France.
DVI ]
François Pottier.
“Typing-by-encoding” -- a reductionistic approach to building type systems, July 2000.
Talk given at IFIP WG 2.8, Seattle, Washington.
PostScript ]