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.