Talks

This page gives a small selection of some of my invited and conference talks:

• Mechanized verification of type systems using Iris.
  At Dagstuhl workshop on behavioral types, January 31, 2024, Dagstuhl, Germany (area keynote).
  
  [slides]
• Interactive and Automated Proofs in Modal Separation Logic.
  At International Conference on Interactive Theorem Proving (ITP), August 2, 2023, Bialystok, Poland (invited talk).
  
  [slides]
• Relational reasoning using concurrent separation logic.
  At EUTypes, February 23, 2019, Krakow, Poland (invited talk).
  At ITU Copenhagen, March 21, 2019, Copenhagen, Denmark.
  At ADSL, January 20, 2020, New Orleans, USA (invited talk).
  
  [slides EUtypes/ITU] [slides ADSL]
• MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic.
  At Inria, September 10, 2018, Paris, France.
  At EUTypes, October 9, 2018, Aarhus, Denmark (invited talk).
  
  [slides Inria] [slides EUTypes]
• Iris Proof Mode: Interactive Proofs in Higher-Order Concurrent Separation Logic.
  At MFPS, June 12, 2017, Ljubljana, Slovenia (invited talk).
  At KULeuven, June 23, 2017, Leuven, Belgium.
  [slides] [coq demo]
• Iris: a framework for higher-order concurrent separation logic in Coq.
  At Type Theory Based Tools (TTT), January 15, 2017, Paris, France (invited talk).
  At UTwente, March 7, 2017, Twente, The Netherlands.
  [slides]
• The C standard formalized in Coq, what’s next?
  At the Cambridge Computer Laboratory, May 13, 2016, Cambridge, UK.
  At Google, April 20, 2016, Aarhus, Denmark.
  At TUDelft, March 9, 2016, Delft, The Netherlands.
  At MPI-SWS, December 15, 2015, Saarbrucken, Germany.
  
  [slides]
• Formalizing C in Coq.
  At Aarhus University, November 17, 2014, Aarhus University, Denmark.
  At the Princeton PL reading group, October 24, 2014, Princeton University, Princeton, USA.
  At ITU Copenhagen, November 11, 2015, Copenhagen, Denmark.
  
  [slides]