Behavioural Types: from Theory to Tools

Behavioural Types: from Theory to Tools

River Publishers Series in Automation, Control and Robotics

Behavioural Types: from Theory to Tools

Editors:
Simon Gay, University of Glasgow, UK
António Ravara, Universidade Nova de Lisboa, Portugal

ISBN: 9788793519824

Available: June 2017

doi: https://doi.org/10.13052/rp-9788793519817


Behavioural type systems in programming languages support the specification and verification of properties of programs beyond the traditional use of type systems to describe data processing. A major example of such a property is correctness of communication in concurrent and distributed systems, motivated by the importance of structured communication in modern software.

Behavioural Types: from Theory to Tools presents programming languages and software tools produced by members of COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems, a European research network that was funded from October 2012 to October 2016. As a survey of the most recent developments in the application of behavioural type systems, it is a valuable reference for researchers in the field, as well as an introduction to the area for graduate students and software developers.
Programming languages; behavioural type systems; choreography; program analysis tools; session types; software contracts; automation

Chapter 1: Contract-Oriented Design of Distributed Applications: A Tutorial
by Nicola Atzei, Massimo Bartoletti, Maurizio Murgia, Emilio Tuosto and Roberto Zunino


930

Chapter 2: Contract-Oriented Programming with Timed Session Types
by Nicola Atzei, Massimo Bartoletti, Tiziana Cimoli, Stefano Lande, Maurizio Murgia, Alessandro Sebastian Podda and Livio Pompianu


931

Chapter 3: A Runtime Monitoring Tool for Actor-Based Systems
by Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir


1389

Chapter 4: How to Verify Your Python Conversations
by Rumyana Neykova and Nobuko Yoshida


1058

Chapter 5: The DCR Workbench: Declarative Choreographies for Collaborative Processes
by Søren Debois and Thomas T. Hildebrandt


996

Chapter 6: A Tool for Choreography-Based Analysis of Message-Passing Software
by Julien Lange, Emilio Tuosto and Nobuko Yoshida


929

Chapter 7: Programming Adaptive Microservice Applications: An AIOCJ Tutorial*
by Saverio Giallorenzo, Ivan Lanese, Jacopo Mauro and Maurizio Gabbrielli


1041

Chapter 8: JaDA – the Java Deadlock Analyzer
by Abel Garcia and Cosimo Laneve


1561

1207

Chapter 10: Session Types with Linearity in Haskell
by Dominic Orchard and Nobuko Yoshida


1144

Chapter 11: An OCaml Implementation of Binary Sessions
by Hernán Melgratti and Luca Padovani


1285

Chapter 12: Lightweight Functional Session Types
by Sam Lindley and J. Garrett Morris


924

Chapter 14: Mungo and StMungo: Tools for Typechecking Protocols in Java
by Ornela Dardha, Simon J.Gay, Dimitrios Kouzapas, Roly Perera, A. Laura Voinea and Florian Weber


999

Chapter 15: Protocol-Driven MPI Program Generation
by Nicholas Ng and Nobuko Yoshida


1059

Chapter 16: Deductive Verification of MPI Protocols
by Vasco T. Vasconcelos, Francisco Martins, Eduardo R. B. Marques, Nobuko Yoshida and Nicholas Ng


1014