When Separation Logic met Java

Separation logic is a promising new approach to modular reasoning, but so far it has primarily been applied to low-level C-like languages. To extend separation logic to allow modular reasoning about object-oriented languages like Java, we must add encapsulation and behavioural subtyping to the logic. However, a naive integration of behavioural subtyping and separation logic is too restrictive. In this talk I will demonstrate how abstract predicate families provide an abstraction mechanism that addresses these restrictions, by mirroring dynamic dispatch in the logic. We demonstrate the utility of our approach with a series of examples, including the Visitor pattern.

Speaker Details

Matthew Parkinson is a Royal Academy of Engineering and EPSRC Postdoctoral Research Fellow in the Computer Laboratory at the University of Cambridge. His fellowship aims to extend Separation Logic to mainstream programming languages such as concurrent Java. He previously working at Middlesex University with Professor Richard Bornat and extended Concurrent Separation logic to reason about non-blocking concurrency. He studied for his thesis at the University of Cambridge under the supervision of Dr. Gavin Bierman and Professor Andrew Pitts/ In October 2005, he successfully defended his thesis on “Local Reasoning in Java”, which extended separation logic to a sequential Java like setting.

Date:
Speakers:
Matthew Parkinson
Affiliation:
University of Cambridge