The contract metaphor is the basis of today’s software verification. Expressing invariants, pre-, and postconditions with logical formulae as part of an interface has become common fare in the construction of dependable software. Often, general logical formulae are replaced by type qualifiers or other abstractions to soften the learning curve.

While traditional contracts focus on characterizing behavior in terms of snapshots by relating the prestate of a function to its poststate, a wealth of recent work has considered behavioral contracts like session types that describe the temporal behavior of program components and/or generalize the notion of the observed state. Often this kind of contract describes the communication behavior of a group of components, but there are many other use cases like typestate reasoning or the description of security policies.

We observed that there are different communities (contracts, sessions, security and typing, specification, and static vs. dynamic verification) that use similar approaches to pursue similar research objectives. Hence, the goal of the seminar is to explore the potential for crossfertilization, to identify commonalities and differences, to get inspiration by discussing the techniques used in the other fields, and to find grounds for future collaboration. The next few paragraphs substantiate this claim by giving very brief outlines of ongoing work in these communities.

Session calculi have been discovered by Kohei Honda in his 1993 paper “Types for Dyadic Interaction”. They extend process calculi with session types that provide a statically checkable (or occasionally dynamically checked), structured means of specifying synchronous communication between two parties. A session type defines the order of the communication actions on a given communication channel and it prescribes the types of the transmitted values.
A session type may specify labeled alternative behaviors and loops, similar to a regular language.
Meanwhile, numerous variations of session calculi have been developed. Some are based on functional and object-oriented calculi. Others include subtyping, asynchronous communication, or they govern multi-party communications. Recent work has established connections with linear logic as a semantic basis for session types and communication automata, which are widely used in the analysis of network protocols.

A closely related line of work considers behavioral types and typestate, where the type of an object changes over time to indicate its current internal state. Methods of the object may be enabled or disabled depending on its current type. The prototypical example is the file that must first be opened, then may be read and written repeatedly, and must finally be closed.

On the other hand, researchers in computer security have considered application monitoring for a long time. A monitor runs alongside the application program and changes state triggered by a stream of events from the running program. If the monitor is used for auditing, then the event stream is condensed to a log and saved for post-mortem analysis. However, the monitor may also be used to enforce a security policy by terminating the program as soon as it attempts to perform an illegal sequence of events.
Most of the time monitoring is performed at run time, but there is also scope for static monitoring. A prime example in this direction is Walker’s “A type system for expressive security policies”, which applies linear and dependent types to express finite state monitoring on the type level.

Recent work indicates that session types and typestate are converging (and some of the convergence is organized in the EU-COST action BETTY), but the situation is less clear for the interaction between session typing and security monitoring. In particular, session typing is mostly considered in a static typing context whereas security monitoring usually happens at run time.
There are only a few exceptions to each, such as Yoshida’s work on run-time enforcement of session types and Walker’s work on a static type system for monitoring. There may even be room for hybrid approaches that apply a mix of static and dynamic checks, in close analogy to existing work in dynamic typing.