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.