Séminaire, 3 avril 2014

Programme

10:30 – 12:00

Emmanouel Beffara (Université d'Aix-Marseille)

Invited talk: A logical view on scheduling in concurrency

This paper elaborates on a new approach of the question of the proof-theoretic study of concurrent interaction called "proofs as schedules". Observing that proof theory is well suited to the description of confluent systems while concurrency has non-determinism 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 prefix-less formalisms (like solos), as the operational counterpart of a translation between logical systems.

• slides

14:00 – 15:00

Giovanni Bernardi (Univ. Lisboa (Portugal))

Invited talk: Mutually testing processes

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 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 multi-linear 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.