PLClub Discussion Group


Separation Types

Aug 21 2020
Paul He

This week I’ll be talking about some work I’ve been doing on formalizing the semantics of a type system called separation types. Separation types is a type system being developed to describe the shape of memory and the capabilities that pointers to it can have. Our approach is based on ideas from separation logic and is meant to allow for type checking to be easily automated. I’ll present some ongoing work on proving the soundness of this type system, using a semantic approach. We represent the types of the language semantically as rely/guarantee relations, building on the idea from previous work that verification techniques for preventing interference in concurrent code is also useful for preventing pointer aliasing.

The homework is to read section 2.3, of Viktor Vafeiadis’s dissertation, at https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf. I won’t be discussing anything too technical, so feel free to skim over the details. If you have more time you can also read the rest of section 2.