Most session type theories focus on enforcing safety properties (nothing “bad” ever happens) with little emphasis on liveness properties (something “good” can or will eventually happen). We are interested in studying liveness properties of multi-party sessions relying on fairness assumptions [CDP11] and the subtyping relations for session types they induce [P11]. Our aim is to design type systems enriched by subtyping that are able to enforce these liveness properties in addition to the traditional safety ones. A combination of induction and coinduction might be necessary in the analysis of such properties. The resulting type systems should be equipped with type checking and type inference algorithms to encourage practical applications.
Previous works have spotted some interesting analogies between sessions and object methods [CCDDG09] and between session types and dynamic object interfaces [GVRGC10]. We plan to introduce aspects [DES10] as an automatic tool for adding correspondence assertions in sessions [BCG05]. As case study we plan to consider the use of remote resources by Android threads.
Currently, global and session types do not account for interleaving of sessions, which are visible only in processes [DLY07, BCDDDY08]. Session interleaving is useful in many scenarios and necessary for delegation. For this reason we are interested in exploring how to enrich the expressivity of global and session types in order to represent session interleaving without decreasing their simplicity and naturalness. The final aim is to study more compositional ways to ensure progress (and possibly liveness) of sessions and to relax some of the constraints imposed by current type systems enforcing global progress properties.
A limit to the use of sessions is the requirement that session types do perfectly match, i.e. they are projections of a global type statically determined, while often the interaction of two or more processes is the result of a negotiation that takes place dynamically, as the processes interact. We plan to study how the possible participants of a session can adapt their behaviors in order to get a successful interaction, replacing a statically pre-defined global type with a dynamic notion of coherence, possibly exploiting the notions of subtype [GH05,BdL10] and exceptions [CGY10]. First steps in this direction, although in a different setting, have been done in [CGP09,P10,CD08,BCDM11]. It appears feasible that these techniques might rely on contract agreement and violation detection mechanisms such as those outlined in [BTZ11].
Most modern computer architectures are based on multiple (possibly heterogeneous) cores that enable, at least in principle, high-performance parallel computations. Taking full advantage of these architectures requires a careful design of algorithms and high-level programming abstractions to tame the complexity of their implementations. We are interested in developing theories of behavioral types to help the design and static verification of multi-core programs on the lines of [YVPH08,HVY09].
There is a plethora of type systems for process calculi that can describe a variety of properties, including authenticity, secrecy and migration properties. An important topic is to find a general framework that will be amenable to automated analyses such as type checking and type inference [HH09].
We are currently working on devising a session type system for understanding the behaviour of field update in object-oriented programs.
We are interested in investigating concurrent global types for multiparty sessions, that is, global types that have a parallel operator in their syntax, like those considered by Pierre-Malo Deniélou and Nobuko Yoshida's in their POPL'11 paper [DY11]. Indeed, in multiparty sessions it does not seem natural to use sequential global types. True-concurrency notions could turn useful here. For instance, would it make sense to describe a behavioural type as some kind of (abstract) event structure, rather than, for instance, a CCS process ?
We plan to pursue the collaborative work started with the Torino group on the integration of security requirements into session calculi, focussing on the property of confidentiality. So far we have investigated a multiparty session calculus enriched with security levels, defined a security property for processes (formalising the preservation of data confidentiality), and shown that an enriched session type system for this calculus, which introduces new requirements for access control and secure information flow, ensures protection of data confidentiality during session execution. This work was presented in [CCDR10], and has since been revised and extended in [CCD11a]. In a subsequent paper [CCD11b], we have moved one step further by equipping the above calculus with a monitored semantics, which blocks the execution of processes as soon as they attempt to leak information. We have shown that the safety property induced by this monitored semantics implies the security property of [CCD11a]. The follow-up of this work could be two-fold:
a) Investigate a labelled version of the monitored semantics, where labels provide informative error messages to the programmer. This labelled monitored semantics could be used either to localise programming errors in order to facilitate their recovery, or to dynamically filter out benign errors, thus avoiding them to block the execution of the whole process. In this case, labels corresponding to benign errors could be recorded in the history of the process and the execution would be allowed to go on, postponing error analysis to the next natural breaking point (e.g., the end of a session).
b) Further explore the relationship between session types and “termination leaks”. Termination leaks are one of the main causes of insecure information flow in a concurrent scenario. These leaks are due to the possibility of different termination behaviours in the branches of a high conditional. In our session calculus above, there are three possible termination behaviours: termination, deadlock and divergence. A termination leak may occur for instance if one branch of a high conditional terminates while the other diverges or deadlocks, since the terminating action may be used to trigger a parallel process which performs some low action. Now, session types may help controlling this phenomenon, because they impose a uniform termination behaviour in conditional branches. Indeed, classical session types already exclude some combinations of termination behaviours in conditional branches. For instance, they rule out a conditional with two non trivial branches one of which terminates while the other diverges. Moreover, session types prevent local deadlocks due to a bad matching of the communication behaviours of different participants in the same session. By adding to classical session types the interaction typing of [BCDDDY08], one may also exclude some global deadlocks due to a bad matching of the protocols of two interleaved sessions. However, this typing still does not prevent deadlocks due to inverted calls to two different services in two parallel processes. We plan to study a strengthening of interaction typing, using the notion of “tester” introduced in [CCD11], in order to rule out also this kind of deadlock. As a result, a well-typed process would be completely free of termination leaks.
We started investigating a notion of reputation for principals participating in multirole sessions (sessions where there may be a varying number of participants for each role, as defined by Deniélou and Yoshida in [DY11]). This is currently the object of collaborative work with the Torino group, and a first outcome is presented in [BCCD11]. The aim is to accomodate dynamic interaction policies in sessions with a varying number of participants, taking into account the reputation of principals. The reputation of a principal is based on her previous behaviour as a user (participant) of a service. A principal's reputation may be checked both by the service itself, before admitting again that principal as a participant, or by another principal to evaluate the reputation of the current participants before she joins the service. We plan to apply this idea to refine our previous work on information flow control in multiparty sessions, by considering reputations built on the “security behaviour” of principals.
* [CCDR10] Sara Capecchi, Ilaria Castellani, Mariangiola Dezani Ciancaglini & Tamara Rezk: Session Types for Access and Information Flow Control. In: Proc. CONCUR’10, LNCS 6269: 237–252, 2010.
* [CCD11a] Sara Capecchi, Ilaria Castellani & Mariangiola Dezani Ciancaglini: Typing Access Control and Secure Information Flow in Sessions. Submitted for journal publication.
* [CCD11b] Sara Capecchi, Ilaria Castellani & Mariangiola Dezani Ciancaglini: Information Flow Safety in Multiparty Sessions. In: Proc. EXPRESS'11, EPTCS 64: 16-30, 2011.
* [BCCD11] Viviana Bono, Sara Capecchi, Ilaria Castellani & Mariangiola Dezani Ciancaglini: A reputation system for multirole sessions. In: Proc. TGC'11, LNCS, to appear.
* [DY11] Pierre-Malo Deniélou & Nobuko Yoshida: Dynamic multirole session types. In Proc. POPL 2011: 435-446, 2011.
Behavioural types are mostly employed to account for functional properties of system behaviour (e.g. safety and liveness properties), while ignoring any non-functional aspect. Such aspects clearly vary depending on the kind of applications: they might represent the cost of acquisition of a resource, the probability/rate of resource consumption, the cost of a method call in oo languages, the quantity of enzyme consumed in a chemical reaction, the level of trust of a participant in an interaction, the rate of leakage of information in a communication or method execution, and so on. We could contribute by defining a theory of quantitative behavioural types, viewed as an abstract operational model accounting for non-functional aspects of the system's behaviour. This means:
We aim at being as general as possible; hence our framework should be quite permissive as to the nature of weights. An interesting possibility seems to take an abstract view of weights as elements of a semiring (see e.g. [1]). In essence, this would amount to viewing systems and behavioural types as weighted automata [1], of which e.g. ordinary and probabilistic transition systems and Markov chains are instances.
[1] Droste, M., Kuich, W., and Vogler, H.: Handbook of Weighted Automata. Springer.
We want to develop a contract refinement/choreography compliance theory encompassing evolvability mechanisms like those modeled in [BDPZ11], i.e. where dynamic update primives can change a specific part (identified by an evolvability hook) of the behaviour of components/services at run-time.
We want to continue the study of the relation between choreography and orchestration for system description, in the style of [CHY07] or [LGMZ08], with particular attention on the possibility of automatically deriving well behaved orchestrations from choreographies. The approaches in the literature require conditions on the form of the choreographies. We want to minimize them as far as possible, and to study techniques for amending choreographies which are not well formed while preserving their intended behavior. We want to apply these techniques also in the object oriented framework. In particular, we want to define choreographies for object oriented systems, and automatically derive contracts specifying the order in which methods of objects can be invoked.
We want to study choreographic specifications for error recovery in distributed systems. In particular, we want to combine the results from [CHY08], with our studies on dynamic compensations and automatic fault notification [CLMZ08]. In this way, participants would be able to ask remote compensations for undoing complex interactions. A possible case study would be to extend with distribution aspects the techniques for reversibility in [LMS10].
We have worked on the design of the sessions concept for object-oriented languages [DDMY09], culminating into a deep amalgmation of the concept of method and session [CCDG09]. We have worked on various approaches to concurrency [DPBE05], we proposed the concept of object change to describe coordination [DGGD08] - a precursor to type classes. We now want to work on the best amalgamation of concurrency, sessions and objects.
We have worked on multi-role session types [GSDW09,R10], and we now want to amalgamate with the concepts of relationship and role, as being developed in oo languages [BG11].
We are currently studying the relationship between session types and contracts for web services. We have two aims; the first is to give an operational semantics to session types, so as to use them as protocol specifications. Our second aim is to assign contracts to processes written in languages such as the picalculus, CaSPiS, the higher-order order picalculus, so that contracts will mirror the behavioural properties of their processes.
[BH11] Modelling session types using contracts. Giovanni Bernardi, Matthew Hennessy; Technical report, TCS-CS-2011-07, Aug 2011, University of Dublin, Trinity College
I am interested in applying “semantic subtyping” techniques [FCB08] to devise and study behavioural types theories on the lines of what already done in [CGP09] and [CDGP09]. The aim is then to experiment and apply, whenever possible, the theoretical results in a pratical framework: in particular I am thinking of OcCduce [OCCDUCE] a web devevelopment system that combines the programming features of a language based on semantic subtyping (ie, CDuce) into a development system for active web applications (ie, Ocsigen).
We want to develop flexible typed process models supporting dynamic adaptation/evolution and distribution. Part of the work will be based on declarative process models developed in [HM10] and [HMS11a-d] jointly with our industrial partners Exformatics A/S and Resultmaker A/S in current nationally funded research projects.
Moreover, we want to develop a theory for evolvable typed process languages based on Milners meta-process theory of Bigraphical Reactive Systems and our previous work on types [EHS08], sortings [BDH06,BDH08] and refinement [PDH11] for bigraphs.
The aim of this project, funded by the Danish Agency for Science, Technology and Innovation, is to provide mathematical foundations for choreography-driven programming (choreography as a programming language for programming distributed systems globally) covering realistic communication and security protocols and supporting algorithms for provable correct mappings between choreography and end-points.
We want to explore logical reasoning for choreographies with the aim to provide a methodology for specification and verification of structured communications. We aim at developing further the work undertaken in [CGHL10] by including choreographies with multiparty sessions [CM12] and investigate how it could be related to the work in [BHTY10].
We wish to investigate further the work developed in [CHY08] and [C08] possibly in collaboration with the Bologna unit and their work on dynamic compensations and automatic fault notification [CLMZ08].