\documentclass[a4paper,article]{memoir}
\title{WG: The Foundations of Behavioural Types}
\author{The BETTY contributors \\ (Compiled by Hans H\"{u}ttel)}
\begin{document}
\maketitle

\chapter{The main research areas}

We here identify 2 main strands of work:

\begin{itemize}
\item Type idioms and type systems for (process) calculi/languages: 
\begin{itemize}
\item Binary session types
\item Multiparty session types
\item Automata-based types
\item Contracts
\item Expressing safety and liveness properties
\end{itemize}
\item Semantic foundations: 
\begin{itemize}
\item Relating approaches via encodings
\item Linear logic
\item Notions of subtyping
\end{itemize}
\end{itemize}



\chapter{Type idioms and type systems}

\section{Dyadic session types}

The paper \cite{DBLP:conf/concur/Honda93} introduced the basic ideas for session types, and \cite{DBLP:conf/esop/HondaVK98} was instrumental to the approach becoming so important.


\section{Multiparty session types}

An important strand of work is that of multiparty session types. The seminal paper is \cite{hondaPOPL} which introduces the notions of local and global descriptions of a system along with local and global types. This work introduces the notion of projection from global types to endpoint types for the asynchronous case.

Later work studies the synthesis of the local from the global and vice versa. \cite{SEFM08} shows that different conditions are needed to make a choreography projectable onto single participants according to whether the semantics is synchronous or asynchronous and, in the asynchronous case, on whether one is interested in the order of send, of receive, or of both.

\subsection{Global descriptions and types}

\cite{DBLP:conf/concur/LangeT12} proposes a typing systems which allows, under some conditions, to synthesise a choreography (i.e. a multiparty global type) from a set of local session types which describe end-point behaviours (i.e. local types).

\cite{DBLP:journals/corr/abs-1203-0780} presents a new, streamlined language of global types equipped with a trace-based semantics, whose features and restrictions are semantically justified.  The paper also provides an extensive comparison with related specification languages adopted in different communities.

\cite{Carbone:2012:SCP:2220365.2220367} introduces global types as descriptions of whole conversation scenarios and relates them to session types.

In \cite{DBLP:conf/popl/CarboneM13} a purely-global programming model is proposed. The authors develop a typing discipline that verifies choreographies against protocol specifications, based on multiparty sessions. Exploiting the nature of global descriptions, our type system defines a new class of deadlock-free concurrent systems (deadlock-freedom-by- design), provides type inference, and supports session mobility. 

\cite{bocchiDATA}  shows how to add data to the theory of choreographies. In particular the paper introduces assertions on the communicated values and invariants for recursion.

\cite{BocchiAMEND} -- Designing well-formed choreographies in the framework introduced in~\cite{bocchiDATA} is not easy. This paper proposes algorithms to help designers in their task, discuss their suitability, and sketch a methodology based on the proposed algorithms.

\cite{DBLP:journals/tcs/CairesV10} introduces a generalisation of session types for multiparty interaction, unifying "local" and "global" types at the same level in the type language and defining a way to distribute "slices" of the protocol in a compositional way, which allows us in particular to address conversations between an unanticipated number of participants.


\cite{brusas} mainly deals with how to correctly instrument monitors for enforcing session types in a distributed setting.  They also provide specification of "located process conformance" to a monitor's specification using bisimulation equivalence.

\section{Contracts}

Contracts take a different approach to behavioural types, using CCS-like languages for describing an abstraction of the behaviour of a program.

In \cite{DBLP:journals/toplas/CastagnaGP09} the authors describe a theory of contracts that formalizes the compatibility of a client with a service, and the safe replacement of a service with another service. \cite{CastagnaPadovani09} explores a contract-based approach for the analysis of distributed systems with dynamic communication topologies.

\cite{DBLP:conf/coordination/BartolettiTZ12} presents a calculus of contracting systems, allowing distributed participants to advertise behavioural contracts, reach agreements and realise them (or choose not to - unlike in traditional approaches based on behavioural types).  The paper introduces the notion of `honesty'' (i.e. the ability of a participant to always realize its advertised contracts, in any context) and proves it to be undecidable.

An important notion is that of \emph{conformance} of a program to a contract. \cite{DBLP:conf/soco/BravettiZ07} presents a foundational theory of behavioural contracts for multi-party service composition, focusing on the conformance relation of a contract for a given role with respect to a (well-formed) choreography. \cite{DBLP:conf/sfm/BravettiZ09} presents a foundational theory of behavioural contracts for multi-party service composition, focusing on contract refinement (coarsest subcontract relation) and its relationship with (fair) testing. 

\section{Interface automata}

Interface automata give an automaton-based approach to behavioural types. The interface of a component is described using an I/O-automaton, and a notion of \emph{refinement} compares abstract and concrete descriptions of a given interface.

 \cite{DBLP:journals/fac/LeeX04} the authors use of interface automata to devise a behavioral type system for Ptolemy II (a software framework for concurrent component composition), that captures the interaction dynamics in a component-based design environment. The interaction types and component behavior are described by interface automata, and type checking is done through automata composition.

\cite{mcm09:ip} proposed a method to enrich the interface automata formalism, which specifies components protocols, by the semantics of actions in order to verify components compatibility and components substitutability at the levels of signatures, semantics, and actions protocols.

\cite{cmm10:ip} presented a formal approach based on interface automata approach and protocols specifications, to adapt components in order to eliminate possible behavioural mismatches, that occur during their interactions.  This approach insures reuse of components in diverse situations without affecting their codes.

\cite{ChoualiH11} describes an approach which combines component SysML models and interface automata in order to assemble components and to verify formally their interoperability. 

\section{Reasoning about properties}

A main motivation for behavioural types has been to capture safety and liveness properties. 
The paper \cite{2008} introduces a type system to prove progress properties for a system in which  sessions can be interleaved in the same processes allowing strong interactions between them.

In the study of liveness properties, \cite{DBLP:journals/iandc/Kobayashi02} shows how to use a notion behavioural types very similar to session types to reason about global properties of systems, in particular lock-freedom.

%A new version of the paper with a revised and deeper notion of progress can be found in http://www.di.unito.it/~padovani/Papers/CoppoDezaniYoshidaPadovani13.pdf.    

\section{Typestates}

Typestates are an older notion of behavioural type in which the type of a typable entity is state-based, with the state describing the operations that are permitted for an object having this particular typestate. The paper \cite{DBLP:conf/popl/GayVRGC10} provides an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e. objects that dynamically change the set of available methods.

\chapter{Semantic foundations}

\section{Subtypin}

\subsection{Subtyping for session types}

\cite{DBLP:journals/acta/GayH05} is a seminal paper, that has opened a new perspective in the setting of session types. This paper makes it possible to think of subtyping as a way of giving semantics to session types. \cite{Barbanera-deLiguoro:PPDP10} proposes a refinement and a simplification of the behavioural semantics of session types, based on the concepts of compliance and sub-behaviour from the theory of web contracts.

\cite{Padovani11c} is a promising and intriguing way to extend the notion of subtyping from dyadic to multiparty sessions.

\cite{Padovani11b} shows the connection between choice operators in session types and intersection and union types in conventional (i.e. non-behavioural) type systems.

\subsection{Relating contracts}

The notion of subtyping has its counterpart in the study of contracts. Using an adapted testing-based equivalence, the authors of \cite{Castagna:2009:CMP:1611711.1611728} provide a semantic account of how to relate contracts, in terms of the eventual outcome (deadlock, success or indefinite progress) of every sub-component making up the contract.

\subsection{Linear logic}

\cite{DBLP:conf/concur/CairesP10} develops a Curry-Howard interpretation between binary session types and linear logic propositions. As linearity is an important and recurring theme in (behavioral) type systems for process calculi, this paper may be one basis for setting clean, robust foundations for modern behavioral type systems.

\section{Relating approaches}

An obvious question to ask is how the type idioms are related. The paper \cite{DBLP:conf/sac/BernardiH12} gives a comparison of session types and contracts.

There is also work on relating session types to standard type systems for the $\pi$-calculus. \cite{DBLP:conf/concur/DemangeonH11} establishes a relationship between (dyadic) session types in the $\pi$-calculus and standard type systems for pi. And\cite{DBLP:conf/ppdp/DardhaGS12} presents a fully abstract translation of session types into a version of the simply typed $\pi$-calculus. This work introduces a theory of subtyping for the $\pi$-calculus, which allows the authors to related (dyadic) session types to more standard typing constructs for the $\pi$-calculus. 

\cite{huttel2011} presents a general type system for psi-calculi that also allows for instantiations to type/effect systems, including a version of Gordon and Jeffrey's system for correspondence types.




\bibliographystyle{plain}
\bibliography{betty-wg1}
%\cite{*}
\end{document}
