Seminars

  • Multiparty Sessions based on Proof Nets

    Dimitris Mostrous

    FCUL

    Abstract: 

    We interpret Linear Logic Proofs (Proof Nets) in a process language based on Solos calculus. The language includes a synchronisation mechanism, obtained by a conservative extension of the logic, that enables to define non-deterministic behaviours and multiparty sessions. Typed terms are strongly normalising, which is the first result of this kind for multiparty interactions.
    From the programming perspective, our proposal provides a logically founded approach to multiparty sessions; from the logic perspective, our contribution fits the challenging theme of a "Curry-Howard" correspondence for concurrency.

    This work was presented in PLACES 2014, and is available at http://www.di.fc.ul.pt/~dimitris/Multiparty_Nets_PLACES14.pdf

    Where: 
    6.3.38
    When: 
    Wednesday, June 25 2014
    Time: 
    13:30
  • Communication contracts for MPI-like languages

    Vasco T. Vasconcelos

    FCUL

    Abstract: 

    We present a notion of dependent types that abstracts the communication part of Message Passing Interface (MPI) -like programs. Such types are naturally equipped with a reduction relation and we show that types do not get stuck. We then move to describe a core programming language whose terms inhabit types. We show that programs do not get stuck, crucially relying on the homonymous result for types. We finally describe a framework for checking the conformance of C+MPI programs against types, relying on the VCC tool.
    [Joint work with Francisco Martins, Eduardo Marques, Nobuko Yoshida, Nicholas Ng]

    Where: 
    6.3.5
    When: 
    Tuesday, May 20 2014
    Time: 
    16:30
  • Mutually testing processes

    Giovanni Bernardi

    FCUL

    Abstract: 

    In the standard testing theory of DeNicola-Hennessy one process is considered to be a refinement of another if every test guaranteed by the former is also guaranteed by the latter. In the domain of web services this has been recast, with processes viewed as servers and tests as clients. In this way the standard refinement preorder between servers is determined by their ability to satisfy clients.

    But in this setting there is also a natural refinement preorder between clients, determined by their ability to be satisfied by servers. In more general settings where there is no distinction between clients and servers, but all processes are peers, there is a further refinement preorder based on the mutual satisfaction of peers.

    In this talk we explain the notions sufficient to give uniform behavioural characterisations of all three preorders. We focusing in particular on the characterisation of the client preorder.

    Where: 
    6.3.38
    When: 
    Wednesday, March 26 2014
    Time: 
    10:00
  • Affine Sessions

    Dimitris Mostrous

    FCUL

    Abstract: 

    Session types describe the structure of protocols from the point of view of each participating channel. In particular, the types describe the type of communicated values, and also the dynamic alternation of input and output actions on the same channel, by which a protocol can be statically verified. Crucial to any term language with session types is the notion of linearity, which guarantees that channels exhibit exactly the behaviour prescribed by their type. We relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.

    Where: 
    6.3.5
    When: 
    Wednesday, March 19 2014
    Time: 
    10:00
  • Using higher-order contracts to model session types

    Giovanni Bernardi

    FCUL

    Abstract: 

    Session types are used to describe and structure interactions between independent processes in distributed systems. Higher-order types are needed to properly structure delegation of responsibility between processes.

    In this talk we show that a sublanguage of higher-order web-service contracts provides a fully-abstract model of recursive higher-order session types. The model is set-theoretic, in that the meaning of a contract is the set of contracts with which it complies. The proof of full-abstraction depends on the novel notion of complement of a contract. We show that the new notion lets us type more well-formed programs than the commonly used type duality does, thereby improving existing type systems.

    Where: 
    6.3.38
    When: 
    Wednesday, March 12 2014
    Time: 
    10:00
Subscribe to Seminars