BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Benjamin Kaminski (University College London) DTSTART:20210217T140000Z DTEND:20210217T150000Z DTSTAMP:20260423T021048Z UID:OWLS/21 DESCRIPTION:Title: Qu antitative Separation Logic\nby Benjamin Kaminski (University College London) as part of Online Worldwide Seminar on Logic and Semantics (OWLS)\ n\n\nAbstract\nWe present quantitative separation logic (QSL). In contrast to classical separation logic\, QSL employs quantities which evaluate to real numbers instead of predicates which evaluate to Boolean values. The c onnectives of classical separation logic\, separating conjunction and sepa rating implication\, are lifted from predicates to quantities. This extens ion is conservative: Both connectives are backward compatible to their cla ssical analogs and obey the same laws\, e.g. modus ponens\, adjointness\, etc. Furthermore\, we present a weakest precondition calculus for quantita tive reasoning about probabilistic pointer programs in QSL. This calculus is a conservative extension of both Ishtiaq's\, O'Hearn's and Reynolds' se paration logic for heap-manipulating programs and Kozen's / McIver and Mor gan's weakest preexpectations for probabilistic programs. Our calculus pre serves O'Hearn's frame rule\, which enables local reasoning - a key princi ple of separation logic. Finally\, we briefly touch upon open questions re garding lower bounds on weakest preexpectations and intensional completene ss of our calculus.\n LOCATION:https://researchseminars.org/talk/OWLS/21/ END:VEVENT END:VCALENDAR