PADOVANI , Luca

No description

We study a natural notion of compliance between clients and services in terms of their bpel (abstract) descriptions. The induced preorder shows interesting connections with the must preorder and has normal form representatives that are parallel-free finite-state activities, called contracts. The preorder also admits the notion of least service...

Deadlock analysis of concurrent programs that contain coordination primitives (wait, notify and Open image in new window ) is notoriously challenging. Not only these primitives affect the scheduling of processes, but also notifications unmatched by a corresponding wait are silently lost. We design a behavioral type system for a core calculus...

We investigate the termination problem in a calculus of sessions with probabilistic choices. In this setting, a whole range of termination properties can be defined, from the weaker almost-sure termination to strong almost-sure termination, passing through positive almost-sure termination. We present two similar session type systems closely...

To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard π-calculus by means of a suitable encoding. The encoding allows one to reuse results about the π-calculus in the context of session-based communications, thus deepening the understanding of...