BEGIN:VCALENDAR
VERSION:2.0
PRODID:icalendar-ruby
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:Europe/Vienna
BEGIN:DAYLIGHT
DTSTART:20210328T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:20201025T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260406T042349Z
UID:1607950800@ist.ac.at
DTSTART:20201214T140000
DTEND:20201214T150000
DESCRIPTION:Speaker: Derek Dreyer\nhosted by Thomas Henzinger\nAbstract: Ir
 is is a framework for higher-order concurrent separation logic\, implement
 ed in the Coq proof assistant\, which we have been developing since 2014.
   Originally designed for pedagogical purposes\, Iris has grown into a on
 going\, multi-institution project\, with active collaborators at Aarhus Un
 iversity\, BedRock Systems\, Boston College\, CNRS/LRI\, Groningen Univers
 ity\, 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-th
 eory in Rust\, Go\, OCaml\, Scala\, and more (https://iris-project.org). 
 In this talk\, we will present two brand new -- and very different -- deve
 lopments that have the potential to extend the reach of Iris even further.
   The first is a new *ownership-based refinement type system* for C\, whi
 ch supports *automated* verification of C programs while at the same time 
 being *foundational* (producing Iris proofs in Coq).The second is a comple
 te "remodeling" of Iris\, replacing its original step-indexed model with a
  *transfinite* step-indexed model in order to make Iris suitable for verif
 ication of liveness properties. For this talk\, we will not assume any pr
 ior knowledge of Iris.Rather\, we will briefly review the distinguishing f
 eatures of Iris\, and then explain the key insights behind the aforementio
 ned new developments -- and the problems they are solving -- at a high lev
 el of abstraction. The first new development is joint work with Michael S
 ammler\, Rodolphe Lepigre\, Robbert Krebbers\, Kayvan Memarian\, and Deepa
 k Garg.  The second is joint work with Simon Spies\, Lennard Gäher\, Dan
 iel Gratzer\, Joseph Tassarotti\, Robbert Krebbers\, and Lars Birkedal. S
 peaker Bio: Derek Dreyer is a tenured faculty member of the Max Planck In
 stitute for Software Systems (MPI-SWS) in Kaiserslautern and Saarbrücken\
 , Germany\, where he leads the “Foundations of Programming” group. He 
 also leads the RustBelt project\, funded by an ERC Consolidator Grant\, wh
 ich investigates the formal properties of Rust\, a new major systems progr
 amming language\, in close collaboration with its developers at Mozilla. D
 erek was awarded the ACM SIGPLAN Robin Milner Young Researcher award in 20
 17\, and\, also in 2017\, distinguished paper awards at each of OOPSLA\, E
 COOP\, and PLDI.
LOCATION:Zoom Link: https://istaustria.zoom.us/j/98682447989?pwd=ZThFV1hYMX
 BpQ2FzVmxUbnVldS9VZz09  (Meeting ID: 986 8244 7989 | Passcode: 192229)\, I
 STA
ORGANIZER:
SUMMARY:Derek Dreyer: Turning Iris Up to Eleven: Next Steps in Higher-Order
  Separation Logic
URL:https://talks-calendar.ista.ac.at/events/2993
END:VEVENT
END:VCALENDAR