On December 19, as part of a workshop in Glasgow of the ABCD project,  António Ravara gave a talk on Behavioural Types for Memory Safety in Mungo.

Abstract

We present a type-based analysis that ensures memory safety and object protocol completion in the language Mungo, a non-trivial subset of Java including generics. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis combines controlling the order in which methods are called by usage checking with a static check that determines if references contain null values. This interdependence yields a refined static analysis: type-safety not only ensures the absence of null pointer dereferencing and memory leaks, a safety property, but also that the intended usage protocol of each object is respected and completed, a liveness property. The type system is implemented in the form of a typechecker in Haskell.

[Slides]