Séminaire, April 3, 2014
Programme
 10:30 – 12:00

Emmanouel Beffara (Université d'AixMarseille)Invited talk: A logical view on scheduling in concurrency
This paper elaborates on a new approach of the question of the prooftheoretic study of concurrent interaction called "proofs as schedules". Observing that proof theory is well suited to the description of confluent systems while concurrency has nondeterminism as a fundamental feature, we develop a correspondence where proofs provide what is needed to make concurrent systems confluent, namely scheduling. In our core logical system (a variant of multiplicative linear logic), processes and schedulers appear explicitly as proofs in different fragments of the proof language and cut elimination between them does correspond to execution of a concurrent system. This separation of roles suggests new insights for the denotational semantics of processes and new methods for the translation of πcalculi into prefixless formalisms (like solos), as the operational counterpart of a translation between logical systems.
 14:00 – 15:00

Giovanni Bernardi (Univ. Lisboa (Portugal))Invited talk: Mutually testing processes
In the standard testing theory of DeNicolaHennessy 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 are concerned with the behavioural characterisations of the server and the client preorders. Acceptance sets are enough to capture the server preorder, but not the client one. To characterise the client preorder we introduce the notion of "usability", and combine it with the one of acceptance sets. This is enough to characterise also the peer preorder.
 15:30 – 16:30

Fanny He (University of Bath (UK))Invited talk: A characterization of the Taylor Expansion of λterms
The Taylor expansion of λterms, as introduced by Ehrhard and Regnier, expresses a λterm as a series of multilinear terms, which capture bounded computations. Normal forms of Taylor expansions give a notion of infinitary normal forms, refining the notion of Böhm trees in a quantitative setting. We give the algebraic conditions over a set of normal simple terms which characterize the property of being the normal form of the Taylor expansion of a λterm. From this full completeness result, we give further conditions which semantically describe normalizable and total λterms.