LaST-FP: Linear Types and Session Types for Functional Programming/Linearity and Order for Typestate and Session Types

• Applicant: Professor Dr. Peter Thiemann
• Subject Area: Software Engineering and Programming Languages
• Term: since 2018
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 395068988

Behavioral types describe object protocols, that is, objects whose state evolves over time in a way that restricts the admissible sequences of operations on the objects. The evolution of the object's state is visible at compile time and thus amenable to verification and analysis, so that the compiler can guarantee adherence to the protocol. Behavioral types can be instantiated in many different ways to obtain different guarantees from typing, among them generic typestate and session types. Checking a protocol at compile-time becomes difficult in the presence of aliasing, when there are multiple references to the same object. Borrowing, a timely concept popularized by the programming language Rust, is an instance of the same problem where there are explicit operations to create aliases. We want to investigate a new foundation for typestate-oriented programming with borrowing, which is based on transitions instead of states. This point of view is different from most existing work which specifies the state transition of a borrowed resource by giving its input and output state as part of the function type. In contrast, our framework relies on an abstraction of the transition space in the form of an ordered partial monoid. Rather than inventing ad-hoc methods for handling borrows, we rely on the theory of ordered types, a refinement of linear type theory.

• DFG Programme: Research Grants