Skip to content. | Skip to navigation

Behavioural Types for Reliable Large-Scale Software Systems
COST Action IC1201

Navigation

You are here: Home / Meetings / WG/MC Meetings: Sunday 13th April 2014 at ETAPS

WG/MC Meetings: Sunday 13th April 2014 at ETAPS

There will be a BETTY meeting on Sunday 13th April, as part of the post-ETAPS workshops in Grenoble.

Here is information about the meeting venue, from the ETAPS web site. Here is more general information about the ETAPS venue.

Programme

Session 1: 9.00 - 10.30

  • Relating Multiparty and Binary Session Types via Linear Logic
    Jorge Perez, New University of Lisbon (joint work with Luís Caires)
  • Recursive Session Types and Linear Logic
    Garrett Morris, University of Edinburgh
  • A Recursive Type System with Type Abbreviations and Abstract Types
    Keiko Nakata, Institute of Cybernetics, Tallinn University of Technology (joint work with Hyeonseung Im and Sungwoo Park) 

Break: 10.30 - 11.00

Session 2: 11.00 - 12.30

  • Typing Liveness in Multiparty Communicating Systems
    Hugo Vieira, University of Lisbon
  • Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
    Thomas Hildebrandt, IT University of Copenhagen 
  • Types and Effects for Deadlock-Free Higher-Order Concurrent Programs
    Luca Padovani, University of Torino

Lunch: 12.30 - 14.00

Session 3: 14.00 - 15.00

  • Practical Interruptible Conversations
    Rumyana Neykova, Imperial College London
  • Choreographies in the Wild
    Massimo Bartoletti, University of Cagliari 

Session 4: 15.00 - 16.00

  • Discussion of future work within BETTY

Break: 16.00 - 16.30

Management Committee Meeting: 16.30 - 17.30 

  • Everyone can attend, but voting is restricted to MC members.
  • Here is the agenda.
  • Here are the minutes.

 

Abstracts of Talks

  • Relating Multiparty and Binary Session Types via Linear Logic
    Jorge Perez, New University of Lisbon (joint work with Luís Caires)

    I will present recent work in which we propose to analyse multiparty protocols using a type theory for binary sessions. The approach is elementary: it relies on medium processes which characterise the behavior of multiparty protocols, representing global session types in a precise sense. As mediums feature only binary exchanges, revealing formal connections between binary and multiparty communications can be established.
     
  • Recursive Session Types and Linear Logic
    Garrett Morris, University of Edinburgh

    Recent work has linked session type systems with Girard's linear logic LL. While such work has provided for replicated process, it has not accounted for recursive session types or recursive processes. This talk will explore the connection between recursive session types and an extension of LL to include least and greatest fixed points. The resulting system is sufficient to encode many examples of recursive sessions, is terminating, and enjoys race- and deadlock-freedom.
     
  • A Recursive Type System with Type Abbreviations and Abstract Types
    Keiko Nakata, Institute of Cybernetics, Tallinn University of Technology (joint work with Hyeonseung Im and Sungwoo Park) 

    A key idea behind type systems for recursive types is to use syntactic contractiveness, meaning every mu-bound variable occurs only under a type constructor. This syntactic constructiveness guarantees the existence of the unique solution of recursive equations and thus has been considered necessary for designing a sound type system.
    In an advanced type system with recursive types, type parameters, and abstract types, however, we cannot easily define the syntactic contractiveness. I will discuss a subtle interaction between them, which contributed to a bug in the OCaml type system (with the -rectypes option). I then present a new semantic notion of contractiveness for types and signatures using mixed induction and coinduction.
    Presented at ICALP 2013.
     
  • Typing Liveness in Multiparty Communicating Systems
    Hugo Vieira, University of Lisbon (joint work with Luca Padovani and Vasco T. Vasconcelos)

    Session type systems are an effective tool to prove that communicating programs do not go wrong, ensuring that the participantsof a session follow the protocols described by the types. In previous work, we introduced a typing discipline for the analysis of progress in binary sessions. In this talk, we present recent work where we generalize the approach to multiparty sessions following the conversation type discipline, while strengthening progress to liveness. Conversation types allow to discipline interaction in systems where a possibly unanticipated number of multiple participants interact using a single medium of communication. We combine the usual session-like fidelity analysis with the liveness analysis and devise an original treatment of recursive types allowing us to address challenging configurations that are out of the reach of existing approaches.
     
  • Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
    Thomas Hildebrandt, IT University of Copenhagen

    We present the first session typing system guaranteeing response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.
     
  • Types and Effects for Deadlock-Free Higher-Order Concurrent Programs
    Luca Padovani, University of Torino

    Deadlock freedom is for concurrent programs what progress is for sequential ones: it indicates the absence of stable (i.e., irreducible) states in which some pending operations cannot be completed. In the particular case of communicating processes, operations are inputs and outputs on channels and deadlocks may be caused by mutual dependencies between communications. In this talk we see how to define an effect system ensuring deadlock freedom of higher-order programs that communicate over linear channels. This work falls within the scope of BETTY's Working Group on programming languages, which aims at the integration of behavioral types into mainstream programming languages.
     
  • Practical Interruptible Conversations
    Rumyana Neykova, Imperial College London

    Scribble is a multiparty session-based specification language for modelling application-level protocols. Scribble protocols enjoy safety and liveness properties such as deadlock-freedom and progress between distributed endpoints. To use our language for describing choreographic communications in a large cyberinfrastucture for the oceanography, we have been working with a NSF project, Ocean Observatories Initiative (OOI) over four years. Our aim is to identify a major class of communication patterns via their use cases, and specify them in Scribble. This talk reports our experiences how to push forward our framework into their infrastructure and presents an essential extension of Scribble emerged from their protocols - support of asynchronously interruptible conversations. We expose the underlying theory of our interrupt mechanism, studying its syntax and semantics and its integration in the MPST theory. Asynchronous
    interrupts have proven expressive enough to represent and verify the main classes of communication patterns in OOI, including asynchronous streaming and various timeout-based protocols, without introducing any additional synchronisations.
     
  • Choreographies in the Wild
    Massimo Bartoletti, University of Cagliari

    We investigate the use of choreographies in distributed scenarios where, as in the real world, mutually distrusting (and possibly dishonest) participants may be unfaithful to their expected behaviour. In our model, each participant advertises its promised behaviour as a contract. Participants may interact through multiparty sessions, created when their contracts allow to synthesise a choreography. We show that
    systems of honest participants (which always adhere to their contracts) enjoy progress and session fidelity.