BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Deadlock-Free Separation Logic
DTSTART:20240206T120000
DTEND:20240206T130000
DTSTAMP:20260407T195019Z
UID:3eeaa32768b78f392057f78988341a72252ce8f13fedb3c6e1d16710
CATEGORIES:Conferences - Seminars
DESCRIPTION:Jules Jacobs\, Cornell University\nSubtitle: Linearity yields 
 progress for dependent higher-order message passing\nJoint work with Jonas
  Kastberg Hinrichsen and Robbert Krebbers\n\nAbstract: We introduce a new 
 concurrent separation logic for message passing programs with mutable stat
 e. The key feature of this logic is that it not only guarantees safety\, b
 ut also deadlock freedom\, and does so “for free” by being linear\, wi
 thout requiring any additional proof effort specific to deadlock freedom. 
 The soundness of the logic is proved via a step-indexed model in Coq. As a
  demonstration\, we show that all programs that can be proven to be deadlo
 ck free using linear session types\, can also be proven deadlock free with
  our logic.\n\nSpeaker bio: Jules Jacobs is a postdoctoral researcher at C
 ornell University\, working with Nate Foster and Alexandra Silva. He did h
 is PhD at Radboud University\, under the supervision of Robbert Krebbers a
 nd Stephanie Balzer\, where he worked primarily on type systems and separa
 tion logics for concurrent programming languages.\n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR