LICS on Wednesday, July 14th

09:00‑10:00 Invited Lecture
Chair: Martin Escardo
Location: AT LT4
09:00 Catuscia Palamidessi (INRIA and LIX, Ecole Polytechnique)
Probabilistic Information Flow

In recent years, there has been a growing interest in considering the probabilistic aspects of Information Flow. In this abstract we review some of the main approaches that have been considered to quantify the notion of information leakage, and we focus on some recent developments.

10:30‑12:30 Process Calculi
Chair: Catuscia Palamidessi
Location: AT LT4
10:30 Magnus Johansson, Jesper Bengtson, Joachim Parrow and Björn Victor
Weak Equivalences in Psi-calculi

Psi-calculi extend the pi-calculus with nominal datatypes to represent data, communication channels, and logics for facts and conditions. This general framework admits highly expressive formalisms such as concurrent higher-order constraints and advanced cryptographic primitives. We here establish the theory of weak bisimulation, where the tau actions are unobservable. In comparison to other calculi the presence of assertions poses a significant challenge in the definition of weak bisimulation, and although there appears to be a spectrum of possibilities we show that only a few are reasonable. We demonstrate that the complications mainly stem from psi-calculi where the associated logic does not satisfy weakening.

We prove that weak bisimulation equivalence has the expected algebraic properties and that the corresponding observation congruence is preserved by all operators. These proofs have been machine checked in Isabelle. The notion of weak barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of barbs in all static contexts. We prove that weak barbed equivalence coincides with weak bisimulation equivalence.

11:00 Massimo Bartoletti and Roberto Zunino
A calculus of contracting processes

We propose a formal theory for contract-based computing. A contract is an agreement stipulated between two or more parties, which specifies the duties and the rights of the parties involved therein. We model contracts as formulae in an intuitionistic logic extended with a "contractual" form of implication. Decidability holds for our logic: this allows us to mechanically infer the rights and the duties deriving from any set of contracts. We embed our logic in a core calculus of contracting processes, which combines features from concurrent constraints and calculi for multiparty sessions, while subsuming several idioms for concurrency.

11:30 Christian Eisentraut, Holger Hermanns and Lijun Zhang
On Probabilistic Automata In Continuous Time

We develop a compositional behavioural model that integrates a variation of probabilistic automata into a conservative extension of interactive Markov chains. The model is rich enough to embody the semantics of generalized stochastic Petri nets. We define strong and weak bisimulations and discuss their compositionality properties. The bisimulations are partly oblivious to the probabilistic branching structure, in order to reflect some natural equalities in this spectrum of models. As a result, the standard way to associate a stochastic process to a generalized stochastic Petri net can be proven sound with respect to weak bisimulation.

12:00 Jean Goubault-Larrecq
Omega-QRB-Domains and the Probabilistic Powerdomain

Is there any cartesian-closed category of continuous domains that would be closed under Jones and Plotkin's probabilistic powerdomain construction? This is a major open problem in the area of denotational semantics of probabilistic higher-order languages. We propose to relax the question, and ask for quasi-continuous domains instead. These retain many nice properties from continuous domains. We introduce a natural class of such quasi-continuous domains, which we call $\omega\QRB$-domains. We show that the category $\omega\QRB$ of $\omega\QRB$-domains has a number of pleasing properties: it is closed under the probabilistic powerdomain functor, has all finite products, all bilimits, and is stable under retracts, and even under so-called quasi-retracts. However, at the time being, we do not know whether $\QRB$ is cartesian closed.

14:00‑15:00 Invited Lecture
Chair: Eugenio Moggi
Location: AT LT4
14:00 Vincent Danos (The University of Edinburgh and CNRS)
Abstracting the ODE semantics of rule-based models: exact and automatic model reduction

Rule-based approaches (as in our own Kappa, or the BNG language, or many other propositions allowing the consideration of "reaction classes") offer some means to capture the combinatorial interactions that are typical of molecular biological systems. They afford relatively compact descriptions of cellular interaction networks despite their explosive combinations of complexation and chemical modifications. Unfortunately this same combinatorial blow-up also prevents the use of the ordinary differential semantics of molecular networks. Indeed, in all but the simplest cases the explicit computation and integration of the ordinary differential semantics of a rule set (as implied by mass action law) is unfeasible.<br/> We address in this paper this fundamental problem by proposing a method to extract reduced differential systems from rule-based models. We show that the approach -which is set in the framework of abstract interpretation- is sound in that it generates a reduced system the solutions of which are projections of the solutions of the original system. Importantly: 1) our method does not require the concrete system to be explicitly computed, so it is intensional, 2) nor does it rely on the choice of a specific set of rates for the system to be reduced, so it is symbolic, and 3) when tested on rule-based models of significant size it achieves good compression, so it is also realistic.

15:30‑17:00 Concurrency
Chair: Vincent Danos
Location: AT LT4
15:30 Cosimo Laneve and Antonio Vitale
The Expressive Power of Synchronizations

A synchronization is a mechanism allowing two or more processes to perform actions at the same time.

We study the expressive power of synchronizations gathering more and more processes simultaneously. We demonstrate the non-existence of a uniform, fully distributed translation of Milner's CCS with synchronizations of n+1 processes into CCS with synchronizations of n processes that retains a ''reasonable'' semantics.

We then extend our study to CCS with symmetric synchronizations allowing a process to perform both inputs and outputs at the same time.

We demonstrate that synchronizations containing more than three input/output items are encodable in those with three items, while there is an expressivity gap between three and two.

16:00 Sam Staton and Glynn Winskel
On the expressivity of symmetry in event structures

There is a renewed interest in causal models such as event structures across a variety of areas. Symmetry is an important and natural feature of many processes. At the same time the introduction of a formal treatment of symmetry to causal models boosts their expressivity considerably, both in terms of the maps and universal constructions causal models can support, and the forms of processes and types they can give semantics to. This paper provides technical results establishing a bridge between the mathematically rich but sometimes operationally colourless world of presheaf models for concurrency and the more operationally informative world of causal models. It concentrates on a particular presheaf category, consisting of presheaves over finite partial orders of events. Such presheaves form a model of nondeterministic processes in which the computation paths have the shape of partial orders, and, for instance, the category of event structures embeds fully and faithfully in the presheaf category. It is shown how with the introduction of symmetry event structures represent {\em all} presheaves over finite partial orders. This is in stark contrast with plain event structures which only represent certain {\em separated} presheaves. Specifically a coreflection from the category of presheaves to the category of event structures with symmetry is exhibited. It is shown how the coreflection can be cut down to an equivalence between the presheaf category and the subcategory of {\em graded} event structures with symmetry. Event structures with {\em strong} symmetries are shown to represent precisely all the separated presheaves. Potential applications to the unfolding of higher-dimensional automata and Petri nets, and weak bisimulation on event structures are sketched. The paper briefly sets the results in the context of a broader programme to develop an intensional form of domain theory, for which causal models appear in describing the intensional manner of computation.

16:30 Thomas Ehrhard
A finiteness structure on resource terms

In our paper "Uniformity and the Taylor expansion of ordinary lambda-terms" (with Laurent Regnier), we studied a translation of lambda-terms as infinite linear combinations of resource lambda-terms, from a calculus similar to Boudol's resource lambda-calculus and based on ideas coming from differential linear logic and differential lambda-calculus. The good properties of this translation wrt. beta-reduction were guaranteed by a coherence relation on resource terms: normalization is "linear and stable" (in the sense of the coherence space semantics of linear logic) wrt. this coherence relation. However, such coherence properties are lost when one considers non-deterministic or algebraic extensions of the lambda-calculus (typically the differential lambda-calculus; the algebraic lambda-calculus is an extension of the lambda-calculus where terms can be linearly combined). The submitted paper introduces a "finiteness structure" on resource terms, in the sense of our earlier works on finitess spaces, which are deeply related with the concept of linearly topologized vector spaces introduced by Lefschetz in 1942. This structure will replace coherence in the algebraic case. Not all algebraic lambda-terms can be translated into finitary linear combinations, but we show that second-order typed algebraic lambda-terms can, by a construction similar to Krivine's version of the strong normalization proof for System F.

17:15‑18:20 Coalgebras. Closing
Chair: Phil Scott
Location: AT LT4
17:15 Samson Abramsky
Coalgebras, Chu Spaces, and Representations of Physical Systems

Coalgebras and Chu spaces are widely studied models of computation, with associated logics. We consider a new kind of application: to modelling physical systems, and in particular quantum systems, as a basis for the logical and semantical analysis of quantum information and computation. This raises new challenges for coalgebra: how to accommodate the *contravariance* which arises naturally as we represent both the states and the properties of physical systems; and how to represent the *symmetries* of these systems, which account e.g. for their unitary dynamics. This motivates us to introduce a novel fibrational structure for coalgebra, and also to make new connections betwen coalgebras and Chu spaces.

We introduce a fibrational structure on coalgebras in which contravariance is represented by indexing. We use this structure to give a universal semantics for quantum systems based on a final coalgebra construction. We characterize equality in this semantics as projective equivalence. We also define an analogous indexed structure for Chu spaces, and use this to obtain a novel categorical description of the category of Chu spaces. We use the indexed structures of Chu spaces and coalgebras over a common base to define a truncation functor from coalgebras to Chu spaces. This truncation functor is used to lift the full and faithful representation of the groupoid of physical symmetries on Hilbert spaces into Chu spaces, obtained in our previous work, to the coalgebraic semantics.

17:45 Stefan Milius
A Sound and Complete Calculus for finite Stream Circuits

Stream circuits are a convenient graphical way to represent streams (or stream functions) computed by finite dimensional linear systems. We present a sound and complete expression calculus that allows us to reason about the semantical equivalence of finite closed stream circuits. For our proof of the soundness and completeness we build on recent ideas of Bonsangue, Rutten and Silva. They have provided a ``Kleene theorem'' and a sound and complete expression calculus for coalgebras for endofunctors of the category of sets. The key ingredient of the soundness and completeness proof is a syntactic characterization of the final locally finite coalgebra. In the present paper we extend this approach to the category of real vector spaces. We prove that a final locally finite (dimensional) coalgebra is, equivalently, an initial iterative algebra. This makes the connection to existing work on the semantics of recursive specifications.

18:15 Closing