[madPL] Fwd: OWLS talk today: Derek Dreyer (MPI-SWS) at 2pm UTC

[Justin Hsu <justhsu@xxxxxxxxxxx>]

Starting in 15 minutes!

https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU16aG9wdz09

---------- Forwarded message ---------
From: Alexandra Silva <alexandra.silva@xxxxxxxxx>
Date: Wed, Dec 9, 2020 at 8:26 AM
Subject: OWLS talk today: Derek Dreyer (MPI-SWS) at 2pm UTC
To: <cl-owls@xxxxxxxxxxxxxxx>

Dear all,

In just over five hours, OWLS will hostÂDerek Dreyer (MPI-SWS) giving a talk on  "Turning Iris Up to Eleven: Next Steps in Higher-Order Separation Logic".

The Zoom link is on the homepage:

https://www.cs.bham.ac.uk/~vicaryjo/owls/

Please see below the abstract. I hope to see many of you there!Â

Let me also take the opportunity to announce next week'sÂseminar, which will be the last of 2020:

16 December 2020 (OWLS special Christmas edition). Moshe Vardi, Rice University, Lessons from COVID-19: Efficiency vs Resilience.Â

Best wishes,

Alexandra

Derek Dreyer, MPI-SWS, "Turning Iris Up to Eleven: Next Steps in Higher-Order Separation Logic".Â

Iris is a framework for higher-order concurrent separation logic, implemented in the Coq proof assistant, which we have been developing since 2014. Originally designed for pedagogical purposes, Iris has grown into a ongoing, multi-institution project, with active collaborators at Aarhus University, BedRock Systems, Boston College, CNRS/LRI, Groningen University, INRIA, ITU Copenhagen, KU Leuven, Microsoft Research, MIT, MPI-SWS, NYU, Radboud University Nijmegen, Saarland University, and Vrije Universiteit Brussel, and over 35 published papers studying or deploying Iris for verification of complex programs and programming language meta-theory in Rust, Go, OCaml, Scala, and more (https://iris-project.org).

In this talk, we will present two brand new -- and very different -- developments that have the potential to extend the reach of Iris even further. The first is a new *ownership-based refinement type system* for C, which supports *automated* verification of C programs while at the same time being *foundational* (producing Iris proofs in Coq). The second is a complete "remodeling" of Iris, replacing its original step-indexed model with a *transfinite* step-indexed model in order to make Iris suitable for verification of liveness properties.

For this talk, we will not assume any prior knowledge of Iris. Rather, we will briefly review the distinguishing features of Iris, and then explain the key insights behind the aforementioned new developments -- and the problems they are solving -- at a high level of abstraction.

The first new development is joint work with Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, and Deepak Garg. The second is joint work with Simon Spies, Lennard GÃher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, and Lars Birkedal.