MSc Presentation: Permission-based separation logic for concurrent Scala programs

When: Aug. 27, 2015, 16:00-18:00

Where: HalB 2B

Who: Charl de Leur

Scala is a versatile multi-paradigm general purpose programming language on the Java Virtual Machine, which offers full compatibility with existing Java libraries and code, while providing a multitude of advanced features compared to Java itself.
Permission-based separation logic has proven to be a powerful formalism in reasoning about memory and concurrency in object-oriented programs – specifically in Java , but there are still challenges in reasoning about more advanced languages such as Scala .

Of the features Scala provides beyond Java , this thesis focusses on first class functions and lexical closures. A formal model subset, of Scala is defined, around these features. Using this foundation we present an extension to permission-based separation logic to specify and reason about functions and closures. Furtermore we provide a demonstration and an argument for its use by performing a case study on the Scala actors library.