Johannes Kloos, a fourth-year PhD student at the Max Planck Institute for Software Systems visited the group this week.

Johannes gave a talk to the group about his current research, on Reasoning about event-based concurrency with Asynchronous Liquid Separation Types.

The talk abstract: I will present work on a program logic and associated type system for reasoning about asynchronous programs manipulating shared mutable state. The logic and type system guarantee the absence of races and the preservation of user-specified invariants using a combination of two ideas: refinement types and concurrent separation logic. The logic track ownership of shared state across concurrently posted tasks and allow reasoning about ownership transfer between tasks using permissions. The type system integrated the logic with refinement types to reason about the contents of the heap, in presence of asynchronous tasks. I will first demonstrate the type system on examples from OCaml, and afterwards sketch some preliminary work in applying it to JavaScript.