Dagstuhl Seminar 17051
Theory and Applications of Behavioural Types
( Jan 29 – Feb 03, 2017 )
- Simon Gay (University of Glasgow, GB)
- Vasco T. Vasconcelos (University of Lisbon, PT)
- Philip Wadler (University of Edinburgh, GB)
- Nobuko Yoshida (Imperial College London, GB)
- Andreas Dolzmann (for scientific matters)
- Annette Beyer (for administrative matters)
- Gradual Session Types : article - Igarashi, Atsushi; Thiemann, Peter; Vasconcelos, Vasco T.; Wadler, Philip - New York : ACM, 2017. - 28 pp. - (Proceedings of the ACM on Programming Languages ; 1. 2017 : Article No. 38).
- Microservices : A Language-Based Approach : article in "Present and Ulterior Software Engineering" - Guidi, Claudio; Lanese, Ivan; Mazzara, Manuel; Montesi, Fabrizio - Berlin : Springer, 2017. - pp 217-225.
- Session Types with Linearity in Haskell : book chapter : Behavioural Types: from Theory to Tools, Editors: Simon Gay, Antonio Ravara, River Publishers, eBook ISBN: 9788793519817 - Orchard, Dominic; Nobuko, Yoshida - Gistrup : River Publishers, 2017. - pp. 219 - 241.
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. Session types enable the communication structure of a concurrent or distributed system to be expressed in programming language terms, so that the implementation of communication within a system can be verified by either compile-time typechecking or run-time monitoring, or a combination of both. More generally, behavioural types include typestate systems, which specify state-dependent availability of operations; choreographies, which specify collective communication behaviour; and behavioural contracts, which specify obligations and guarantees on the interaction between agents in a distributed system.
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, gradual typing, dependent type theory, and model-checking. Such work has generated new interest in behavioural type theory among researchers in previously unconnected topics. On the practical side, there are now 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. These language implementations and tools cover a range of paradigms (imperative, functional, object-oriented), communication styles (sockets, MPI, actors) and languages (at least Java, Python, C, Scala, Haskell, Erlang).
The seminar will bring together researchers working on behavioural types in general, session types in particular, and type-theoretical topics such as gradual typing and dependent typing that are becoming increasingly connected to behavioural types. The participants will include those whose research is mainly theoretical, those who are implementing programming languages and tools, and those whose work combines theory and practice.
During the seminar we hope to make progress on at least the following questions:
- 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 modelchecking?
- What are the theoretical and practical obstacles to delivering behavioural types to software developers in a range of mainstream or novel programming languages?
- How can we evaluate the effectiveness of behavioural types in programming languages and software development?
Behavioural types describe dynamic aspects of a program, in contrast to data types, which describe the fixed structure of data. Behavioural types include session types, typestate, choreographies, and behavioural contracts. Recent years have seen a substantial increase in research activity, including theoretical foundations, design and implementation of programming languages and tools, studies of the relationships between different forms of behavioural types, and studies of the relationships between behavioural types and more general type-theoretic ideas such as gradual typing and dependent typing. The aim of this seminar was to bring together researchers on behavioural types and related topics, in order to understand and advance the state of the art.
Many of the participants have been active in COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY), a European research network on behavioural types. Other participants were invited from related research areas and from outside Europe, in order to broaden the scope of the seminar and to make connections between communities.
The programme for the first half of the week was planned in advance, with priority given to two kinds of presentation: (1) demonstrations of programming language implementations and tools, and (2) presentations by participants from outside the BETTY community. The programme for the second half of the week evolved during the seminar, with more emphasis on group discussion sessions.
The seminar was judged to be a success by all the participants. At least one conference submission resulted from collaboration started during the week, other existing collaborations made substantial progress, and several participants planned a submission to the EU RISE funding scheme. We intend to propose a follow-on seminar on a similar topic in the future.
This report contains the abstracts of the talks and software demonstrations, and summaries of the group discussion sessions.
- Gul Agha (University of Illinois - Urbana-Champaign, US) [dblp]
- Nada Amin (EPFL - Lausanne, CH) [dblp]
- Robert Atkey (University of Strathclyde - Glasgow, GB) [dblp]
- Giovanni Tito Bernardi (University Paris-Diderot, FR) [dblp]
- Laura Bocchi (University of Kent - Canterbury, GB) [dblp]
- Edwin Brady (University of St. Andrews, GB) [dblp]
- Luis Caires (New University of Lisbon, PT) [dblp]
- Marco Carbone (IT University of Copenhagen, DK) [dblp]
- Ilaria Castellani (INRIA Sophia Antipolis, FR) [dblp]
- Tzu-Chun Chen (TU Darmstadt, DE) [dblp]
- Mariangiola Dezani (University of Turin, IT) [dblp]
- Patrick Thomas Eugster (TU Darmstadt, DE) [dblp]
- Adrian Francalanza (University of Malta - Msida, MT) [dblp]
- Ronald Garcia (University of British Columbia - Vancouver, CA) [dblp]
- Simon Gay (University of Glasgow, GB) [dblp]
- Philipp Haller (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Thomas T. Hildebrandt (IT University of Copenhagen, DK) [dblp]
- Hans Hüttel (Aalborg University, DK) [dblp]
- Keigo Imai (Gifu University, JP) [dblp]
- Dimitrios Kouzapas (University of Glasgow, GB) [dblp]
- Roland Kuhn (Actyx AG - München, DE) [dblp]
- Ivan Lanese (University of Bologna, IT) [dblp]
- Hugo-Andrés López (Technical University of Denmark - Lyngby, DK) [dblp]
- Francisco Martins (University of Lisbon, PT) [dblp]
- Conor McBride (University of Strathclyde - Glasgow, GB) [dblp]
- Hernán Melgratti (University of Buenos Aires, AR) [dblp]
- Fabrizio Montesi (University of Southern Denmark - Odense, DK) [dblp]
- J. Garrett Morris (University of Edinburgh, GB) [dblp]
- Nicholas Ng (Imperial College London, GB) [dblp]
- Dominic Orchard (University of Kent - Canterbury, GB) [dblp]
- Luca Padovani (University of Turin, IT) [dblp]
- Jovanka Pantovic (University of Novi Sad, RS) [dblp]
- Frank Pfenning (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Antonio Ravara (Universidade Nova de Lisboa, PT) [dblp]
- Konstantinos Sagonas (Uppsala University, SE) [dblp]
- Alceste Scalas (Imperial College London, GB) [dblp]
- Nicolas Tabareau (Ecole des Mines de Nantes, FR) [dblp]
- Peter Thiemann (Universität Freiburg, DE) [dblp]
- Hugo Torres Vieira (IMT - Lucca, IT) [dblp]
- Emilio Tuosto (University of Leicester, GB) [dblp]
- Vasco T. Vasconcelos (University of Lisbon, PT) [dblp]
- Philip Wadler (University of Edinburgh, GB) [dblp]
- Nobuko Yoshida (Imperial College London, GB) [dblp]
- Shoji Yuen (Nagoya University, JP) [dblp]
- programming languages / compiler
- semantics / formal methods
- verification / logic
- behavioural types
- session types
- programming languages
- type systems
- distributed systems
- static analysis
- runtime monitoring