Arnaud Daby-Seesaram.

**Osiris: an iris-based program logic for
OCaml**, September 2023.

Talk given (remote) at the OCaml workshop.

[ PDF ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Talk given at Collège de France, Paris, France. In French.

[ PDF ]

François Pottier.

**Playing spy games in Iris**, November
2019.

Talk given at IFIP WG 2.16, Nice, France.

[ PDF ]

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 ]

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 ]

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 ]

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 ]

Talk given at ESOP 2018, Thessaloniki, Greece.

[ PDF ]

François Pottier.

**Mezzo: an experience report**, December
2017.

Talk given at ENS, Lyon, France.

[ PDF ]

Talk given at ENS, Lyon, France.

[ PDF ]

François Pottier.

**Visitors unchained**, September 2017.

Talk given at ICFP 2017, Oxford, United Kingdom.

[ PDF ]

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 ]

Talk given at IFIP WG 2.8, Edinburgh, Scotland.

[ PDF ]

François Pottier.

**Temporary read-only permissions for
separation logic**, April 2017.

Talk given at Inria, Paris, France.

[ PDF ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Talk given at the OCaml Users meeting, Paris, France.

[ PDF ]

François Pottier.

**Type inference**, August 2015.

Talk given at PLMW @ ICFP 2015, Vancouver, Canada.

[ PDF ]

Talk given at PLMW @ ICFP 2015, Vancouver, Canada.

[ 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 ]

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 ]

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 ]

Talk given at FLOPS 2014, Kanazawa, Japan.

[ 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 ]

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 ]

Talk given at Microsoft Research, Cambridge, UK.

[ PDF ]

François Pottier.

**Types for complexity-checking**, March
2011.

Talk given at ENS, Lyon, France.

[ PDF ]

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 ]

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 ]

Talk given at JFLA 2011, La Bresse, France.

[ PDF ]

François Pottier.

**Hidden state and the anti-frame rule**,
December 2009.

Talk given at Université Paris 7, Paris, France.

[ PDF ]

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 ]

Talk given at Université Paris 7, Paris, France.

[ PDF ]

Arthur Charguéraud.

**Functional translation of a calculus of
capabilities**, September 2008.

Talk given at ICFP 2008, Victoria, Canada.

[ PDF ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Talk given at INRIA, Rocquencourt.

[ PDF ]

François Pottier.

**Static name control for FreshML**, July
2007.

Talk given at LICS 2007, Wroclaw, Poland.

[ PDF ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Course given at the APPSEM Summer School, Frauenchiemsee, Germany.

[ PDF ]

François Pottier.

**Towards efficient, typed LR parsers**,
June 2005.

Talk given in Schloss Dagstuhl, Germany.

[ PDF ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Talk given at IFIP WG 2.8, Seattle, Washington.

[ PostScript ]