Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. In the first part of the talk, I will first present an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs); and a sound characterisation of a subset of safe CFSMs from which global graphs can be constructed. In the second part, I will outline a few recent applications of this work to communicating timed automata and the Go programming language.

We introduce a fully-abstract intensional model for a polymorphic call-by-value language with higher-order references. As in game semantics, the denotation of a term is represented as a set of plays between the term and its environment. But rather than building it compositionally, by induction over the term, we generate it using a labelled transition system representing all the possible interactions between the term and any environment. Names, and more generally the theory of nominal sets, are crucially used to represent locations (i.e. memory addresses) and functional and polymorphic values. Freshness of such names then control the observational power of environments. Thanks to the presence of references, the observational power of environments is strong enough to avoid the need of performing a quotient of the model to be fully abstract. This gives us new principles to reason on effectul and polymorphic programs. This work has been done in collaboration with Nikos Tzevelekos (QMUL).

We study the theory of contextual equivalence in the untyped lambda-calculus, generated by taking the normal forms as observables. Introduced by Morris in 1968, this is the original extensional lambda theory H+ of observational equivalence. On the syntactic side, we show that this lambda-theory validates the omega-rule, thus settling a long-standing open problem. On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for H+. We show that a relational graph model captures Morris's observational pre-order exactly when it is extensional and lambda-König. Intuitively, a model is lambda-König when every lambda-definable tree has an infinite path which is witnessed by some element of the model.

The process of inverting Markov kernels relates to the important subject of Bayesian modelling and learning. In fact, Bayesian update is exactly kernel inversion. ​We investigate how and when Markov kernels (aka stochastic relations, or probabilistic mappings) can be inverted. We address the question both directly on the category of measurable spaces, and indirectly by interpreting kernels as Markov operators: For the direct option, we introduce a typed version of the category of Markov kernels and use the so-called ‘disintegration of measures’. Here, one has to specialise to measurable spaces borne from a simple class of topological spaces -e.g. Polish spaces (other choices are possible). Our method and result greatly simplify a recent development ​by Culbertson and Sturz. For the operator option, we use a cone version of the category of Markov operators (​aka ​kernels seen as predicate transformers). That is to say, our linear operators are not just continuous, but are required to satisfy the stronger condition of being ω-chain-continuous.​ ​Prior work shows that one obtains an adjunction in the form of a pair of contravariant and inverse functors between the categories of L1- and L∞-cones. Inversion, seen through the operator prism, is just adjunction.​ ​No topological assumption is needed. We​ ​show​ ​that​ ​both​ ​categories​ ​(Markov​ ​kernels​ ​and​ ​ω-chain-continuous Markov operators) are related by a family of contravariant functors Tp for 1 ≤ p ≤ ∞. The Tp’s are Kleisli extensions of (duals of) conditional expectation functors introduced ​before. We​ prove​ ​that​ ​both​ ​notions​ ​of​ ​inversion agree when both defined: if f is a kernel, and f† its direct inverse, then T∞(f)† = T1(f†). This is a joint work with Fredrik Dahlqvist UCL, Ohad Kammar Oxford, Ilias Garnier ENS

We introduce a linear infinitary lambda-calculus in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the infinitary applicative lambda-calculus and is universal for computations over infinite strings. What is particularly interesting about the calculus is that the refinement induced by linear logic allows to restrict both modalities so as to get calculi which are terminating inductively and productive coinductively. We exemplify this idea by isolating a fragment of the calculus around the principles of SLL and 4LL. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary lambda-calculi.

The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected.

We propose a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We prove then sound- ness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.

This is a joint work with Mariangiola Dezani-Ciancaglini.

(joint work with Marcelo Fiore and Pierre-Louis Curien)

I will present “linear call-by-push-value” enriched-adjunction models refining call-by-push-value models of effects and linear/non-linear models of linear logic, with higher-order functions, sums, and resource modalities, together with a theorem lifting linear models into cartesian ones. I will also present computational interpretations of these models as intuitionistic (linear) logics (LJ/ILL) where the order of evaluation matters, in the form of polarised calculi that satisfy usual properties of Barendregt-style lambda-calculus, and that have sound and coherent interpretations in the previous models. This suggests an approach to modelling proofs and programs with direct models and calculi.

The purpose of this talk is to explain a new approach to complexity theory based on (dynamic) semantics of linear logic, whose aim is to enable techniques and invariants from ergodic theory (e.g. l^2-Betti numbers of a countable Borel equivalence relation) to be used in computational complexity.

The origins of the techniques can be traced to Girard's “geometry of interaction” (GoI) program using von Neumann algebras and the recent GoI-inspired results in complexity. However, this approach reaches its full strength when using the more combinatorial setting of Interaction Graphs models of (fragments of) linear logic. Using techniques akin to game semantics (with a bit of measure theory), we are able to characterise (predicate) complexity classes as the set of programs/proofs interpretations of type Pred[m] := Nat ⇒ Bool. These models are parametrised by a group of measure-preserving maps m (equivalently, by a measurable group action) and provide the first sketches of a conjectured correspondence between measurable group actions and complexity constraints.

The GHZ and W states are two entangled quantum states of three qubits, that are inequivalent in the sense that one cannot be turned into the other by local (single-qubit) operations; this is reflected in their different communicational properties and use in cryptographic protocols. A few years ago, Coecke and Kissinger showed that one can associate, to the two states, two Frobenius algebras in the category of Hilbert spaces - a type of algebra with a well-understood string diagram representation, which could hopefully provide a bridge between algebraic, computational and topological aspects of quantum entanglement. We present a complete graphical axiomatisation of the relations between the GHZ and W states/algebras: the ZW calculus. This calculus refines the pre-existing ZX calculus, while keeping its most desirable characteristics, such as the undirectedness of diagrams; comes with an explicit normalisation procedure; provides an original decomposition of the category of qubits, with a prominent “fermionic” fragment; and hints at a topological explanation of its components and axioms.