BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Derek Dreyer (Max Planck Institute for Software Systems)
DTSTART:20201209T140000Z
DTEND:20201209T150000Z
DTSTAMP:20260423T052503Z
UID:OWLS/14
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/14/">Tu
 rning Iris Up to Eleven: Next Steps in Higher-Order Separation Logic</a>\n
 by Derek Dreyer (Max Planck Institute for Software Systems) as part of Onl
 ine Worldwide Seminar on Logic and Semantics (OWLS)\n\n\nAbstract\nIris is
  a framework for higher-order concurrent separation logic\, implemented in
  the Coq proof assistant\, which we have been developing since 2014. Origi
 nally 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\, IN
 RIA\, ITU Copenhagen\, KU Leuven\, Microsoft Research\, MIT\, MPI-SWS\, NY
 U\, Radboud University Nijmegen\, Saarland University\, and Vrije Universi
 teit 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).\n\nIn thi
 s talk\, we will present two brand new -- and very different -- developmen
 ts that have the potential to extend the reach of Iris even further. The f
 irst is a new *ownership-based refinement type system* for C\, which suppo
 rts *automated* verification of C programs while at the same time being *f
 oundational* (producing Iris proofs in Coq). The second is a complete "rem
 odeling" of Iris\, replacing its original step-indexed model with a *trans
 finite* step-indexed model in order to make Iris suitable for verification
  of liveness properties.\n\nFor this talk\, we will not assume any prior k
 nowledge of Iris. Rather\, we will briefly review the distinguishing featu
 res of Iris\, and then explain the key insights behind the aforementioned 
 new developments -- and the problems they are solving -- at a high level o
 f abstraction.\n\nThe first new development is joint work with Michael Sam
 mler\, 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.\n
LOCATION:https://researchseminars.org/talk/OWLS/14/
END:VEVENT
END:VCALENDAR