O'Hearn Fest (POPL 2024)
as the organisers put it
A day of talks in celebration of Peter O’Hearn’s scientific and industrial work. Peter is a professor of Computer Science at University College London and an Engineering Director at Lacework. All are welcome, please register to the workshop if you are planning to attend.
| title | author | length |
|---|---|---|
| Introduction | Azalea Raad, Jules Villard | 11m |
Brief history and concrete impact: seminal papers on concurrent separation logic (2004) and the original separation logic paper accumulate major influence —… | ||
| Peter's early work on parametricity, and why it still matters to me | Hongseok Yang | 25m |
Argues that Peter H.'s categorical account of relational parametricity (using reflexive graphs and naturality) gives a formal semantics that validates… | ||
| Strong vs. weak separating conjunction in CSL | James Brotherston | 20m |
Argues that two distinct separations are necessary in concurrent separation logic: a strong separating conjunction for writing inductive/imprecise predicates… | ||
| Verified Software at Scale | Philippa Gardner | 31m |
Mechanized WebAssembly semantics now feed the standard, with a formal DSL that produces parser tests, reference interpreters and automatically generated… | ||
| Later Credits: A Case Study in the Unreasonable Effectiveness of Separation ... | Derek Dreyer | 17m |
Presents a concrete mechanism inside Iris that turns the later modality into an ownable resource called later credits, letting a step produce a credit and… | ||
| Bi-abductive adversarial program synthesis | Julien Vanegue | 22m |
Claims a practical pipeline that uses bi-abduction + deductive synthesis to automatically produce adversary programs that exploit real bugs, demonstrates a… | ||
| CSL and relaxed memory | Stephen Brookes | 21m |
Provides a compositional denotational semantics using pomsets parameterized by a memory model via a relaxation relation and a linearity constraint (row and… | ||
| Is Peter Correct or Incorrect? | Patrick Cousot | 24m |
Claims that incorrectness logic is the dual of Hoare-style total/partial correctness under abstract interpretation and gives a constructive, sound-and-complete… | ||
| Massive proofs for the masses | Byron Cook | 21m |
Claims that cloud-backed distributed solvers dramatically outperform sequential tools—example: a distributed solver reaches ~250 benchmarks solved within 200s… | ||
| Designing Wait-free Weak Reference Counting | Matthew J. Parkinson | 19m |
Claims a wait-free weak reference counting algorithm that lets weak-to-strong promotions terminate regardless of other threads by changing the state machine… | ||
| Elegance and generosity are scientific values - And other things I've learne... | Jade Alglave | 09m |
Begins with a concrete claim: ambitious theory should ship a working artifact — a demo tool that finds surprising bugs in Linux and makes the idea believable… | ||
| Peter, the May and the Must, and Lacework | Patrice Godefroid | 24m |
Lacework builds a cloud-scale security pipeline that combines static SCA of repos and container images, quick buildless source analysis plus deeper info‑flow… | ||
| Working with Peter O'Hearn in academia and industry | Mark Harman | 21m |
[O'HearnFest] Working with Peter O'Hearn in academia and industry
Mark Harman
No description available | ||
| Pete's Footprints | Nick Benton | 19m |
Thirty years of follow-on work traces specific technical moves: an effect system in a Standard ML compiler used to prove correctness of optimizations… | ||
| Symbolic Execution with Separating Decision Diagrams | Josh Berdine | 24m |
Defines separating decision diagrams as a zero-suppressed BDD variant that encodes star/or separation-logic formulas by treating atoms (pure or spatial) as ZDD… | ||
| nothing matches | ||