François Pottier.
Will it fit?, April 2024.
Talk given at IFIP WG 2.8, Utrecht, Netherlands.
[ PDF ]
François Pottier.
Correct, fast LR(1) unparsing,
February 2024.
Talk given at JFLA 2024, Saint Jacut de la Mer, France.
[ PDF ]
François Pottier.
Thunks and debits in Iris with time
credits, January 2024.
Talk given at POPL 2024, London, UK.
[ PDF ]
Arnaud Daby-Seesaram.
Osiris: an iris-based program logic for
OCaml, September 2023.
Talk given (remote) at the OCaml workshop.
[ PDF ]
François Pottier.
Thunks and debits in Iris with time
credits, March 2023.
Talk given at Inria Paris and at Aarhus University.
[ PDF ]
François Pottier.
Current trends in separation logic,
February 2023.
Short informal talk given at ENS, Paris.
[ PDF ]
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 ]