Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051)

Authors Simon Gay, Vasco T. Vasconcelos, Philip Wadler, Nobuko Yoshida and all authors of the abstracts in this report

Thumbnail PDF


  • Filesize: 0.89 MB
  • 32 pages

Document Identifiers

Author Details

Simon Gay
Vasco T. Vasconcelos
Philip Wadler
Nobuko Yoshida
and all authors of the abstracts in this report

Cite AsGet BibTex

Simon Gay, Vasco T. Vasconcelos, Philip Wadler, and Nobuko Yoshida. Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051). In Dagstuhl Reports, Volume 7, Issue 1, pp. 158-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


This report documents the programme and the outcomes of Dagstuhl Seminar 17051 "Theory and Applications of Behavioural Types". Behavioural types describe the dynamic aspects of programs, in contrast to data types, which describe the fixed structure of data. Perhaps the most well-known form of behavioural types is session types, which are type-theoretic specifications of communication protocols. More generally, behavioural types include typestate systems, which specify state-dependent availability of operations; choreographies, which specify collective communication behaviour; and behavioural contracts. In recent years, research activity in behavioural types has increased dramatically, in both theoretical and practical directions. Theoretical work has explored new relationships between established behavioural type systems and areas such as linear logic, automata theory, process calculus testing theory, dependent type theory, and model-checking. On the practical side, there are several implementations of programming languages, programming language extensions, software development tools, and runtime monitoring systems, which are becoming mature enough to apply to real-world case studies. The seminar brought together researchers from the established, largely European, research community in behavioural types, and other participants from outside Europe and from related research topics such as effect systems and actor-based languages. The questions that we intended to explore included: - How can we understand the relationships between the foundations of session types in terms of linear logic, automata, denotational models, and other type theories? - How can the scope and applicability of behavioural types be increased by incorporating ideas and approaches from gradual typing and dependent type theory? - What is the relationship, in terms of expressivity and tractability, between behavioural types and other verification techniques such as model-checking? - What are the theoretical and practical obstacles to delivering behavioural types to software developers in a range of mainstream programming languages? - What are the advantages and disadvantages of incorporating behavioural types into standard programming languages or designing new languages directly based on the foundations of session types? - How can we evaluate the effectiveness of behavioural types in programming languages and software development?
  • Behavioural Types
  • Programming Languages
  • Runtime Verification
  • Type Systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads