http://www.dagstuhl.de/17051

29. Januar – 03. Februar 2017, Dagstuhl Seminar 17051

Theory and Applications of Behavioural Types

Organisatoren

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)


1 / 5 >

Auskunft zu diesem Dagstuhl Seminar erteilen

Annette Beyer zu administrativen Fragen

Andreas Dolzmann zu wissenschaftlichen Fragen

Dokumente

Teilnehmerliste
Gemeinsame Dokumente
Programm des Dagstuhl Seminars [pdf]

Motivation

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?

License
  Creative Commons BY 3.0 DE
  Simon Gay and Vasco T. Vasconcelos and Philip Wadler and Nobuko Yoshida

Classification

  • Programming Languages / Compiler
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Behavioural types
  • Session types
  • Typestate
  • Programming languages
  • Type systems
  • Semantics
  • Concurrency
  • Distributed systems
  • Static analysis
  • Runtime monitoring

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.