Talks

Invited talks and seminar talks

• 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]
• Mechanized proofs in higher-order separation logic.
  At Vrije Universiteit, February 5, 2019, Amsterdam, The Netherlands.
  
  [slides]
• 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]
• Demonstration of the Iris separation logic in Coq.
  At Coq PL, January 21, 2017, Paris, France (invited talk).
  [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]
• Formalization of C: What we have learned and beyond
  At Workshop on realistic program verification, December 2, 2015, Nijmegen, The Netherlands.
  
  [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]
• A Separation Logic for Non-determinism and Sequence Points in C Formalized in Coq.
  At TYPES, May 14, 2014, IHP, Paris, France.
  [slides]
• Moessner's Theorem: an exercise in coinductive reasoning in Coq.
  At the COIN seminar, November 12, 2013, CWI, Amsterdam, the Netherlands.
  [slides]
• Separation Logic for Non-local Control Flow and Block Scope Variables.
  At the Gallium seminar, February 4, 2013, INRIA Rocquencourt, Paris, France.
  [slides]
• Separation Logic for Non-local Control Flow.
  At the Brouwer seminar, November 20, 2012, Radboud University, Nijmegen, the Netherlands.
  [slides]
• Formalizing the C99 standard.
  At ICT.OPEN, November 15, 2011, Veldhoven, the Netherlands (invited talk).
  [slides]
• Type Classes for Efficient Exact Real Arithmetic in Coq.
  At TYPES, September 9, 2011, Bergen, Norway.
  [slides]
• Computer certified efficient exact reals in Coq.
  At the the Coq Workshop, August 26, 2011, Nijmegen, the Netherlands.
  [slides]
• Computer certified efficient exact reals in Coq.
  At the Brouwer seminar, March 22, 2011, Radboud University, Nijmegen, the Netherlands.
  [slides]
• Type Classes for Mathematics.
  At the Workshop on reification and generic tactics, March 31, 2011, INRIA, Paris, France.
  [slides]

Conference and workshop talks

• MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic (with Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud and Derek Dreyer).
  At ICFP, September 25, 2019, St. Louis, USA.
  [slides] [paper]
• The Essence of Higher-Order Concurrent Separation Logic (with Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer and Lars Birkedal).
  At ESOP, April 18, 2017, Uppsala, Sweden.
  [slides] [paper]
• Interactive Proofs in Higher-Order Concurrent Separation Logic (with Amin Timany and Lars Birkedal).
  At POPL, January 18, 2017, Paris, France.
  [slides] [paper]
• A Typed C11 Semantics for Interactive Theorem Proving (with Freek Wiedijk).
  At CPP, January 13, 2015, Mumbai, India.
  [slides] [paper]
• Separation algebras for C verification in Coq.
  At VSTTE, July 18, 2014, Vienna, Austria.
  [slides] [paper]
• Formal C semantics: CompCert and the C standard (with Xavier Leroy and Freek Wiedijk).
  At ITP, July 17, 2014, Vienna, Austria.
  [slides] [paper]
• An operational and axiomatic semantics for non-determinism and sequence points in C.
  At POPL, January 22, 2014, San Diego, USA.
  [slides] [paper]
• Aliasing restrictions of C11 formalized in Coq.
  At CPP, December 11, 2013, Melbourne, Australia.
  [slides] [paper]
• Separation Logic for Non-local Control Flow and Block Scope Variables (with Freek Wiedijk).
  At FoSSaCS, March 19, 2013, Rome, Italy.
  [slides] [paper]
• A call-by-value λ-calculus with lists and control.
  At CL&C, July 08, 2012, Warwick, United Kingdom.
  [slides] [paper]
• Computer certified efficient exact reals in Coq (with Bas Spitters).
  At CICM, July 22, 2011, Bertinoro, Italy.
  [slides] [paper]
• A Formalization of the C99 Standard in HOL, Isabelle and Coq (with Freek Wiedijk).
  At CICM, July 19, 2011, Bertinoro, Italy.
  [slides] [paper]
• Pure Type Systems without Explicit Contexts (with Herman Geuvers, James McKinna and Freek Wiedijk).
  At LFMTP, July 14, 2010, Edinburgh, United Kingdom.
  [slides] [paper]