# Program

### Monday, July 3

__10:00 - 10:30 : coffee break + viennoiseries__- 10:30 - 12:00 : Rasmus Møgelberg (I) (slides)
__12:00 - 14:00 : lunch__- 14:00 - 15:00 : Jurriaan Rot (I)
__15:30 - 15:45 : break__- 15:30 - 16:30 : Alexis Saurin

### Tuesday, July 4

__09:00 - 09:30 : coffee break + viennoiseries__- 09:30 - 11:00 : Neil Ghani (I)
__11:00 - 11:15 : break__- 11:15 - 12:15 : Valeria Vignudelli (slides)
__12:15 - 14:00 : lunch__- 14:00 - 15:30 : Henning Basold (I)
__15:30 - 15:45 : break__- 15:45 - 16:45 : Luigi Santocanale

### Wednesday, July 5

__09:00 - 09:30 : coffee break + viennoiseries__- 09:30 - 11:00 : Rasmus Møgelberg (II) (slides, assignments)
__11:00 - 11:15 : break__- 11:15 - 12:15 : Niccolò Veltri
__12:15 - 14:00 : lunch__- 14:00 - 15:30 : Jurriaan Rot (II)
__15:30 - 15:45 : break__- 15:45 - 16:45 : Rodolphe Lepigre

### Thursday, July 6

__09:00 - 09:30 : coffee break + viennoiseries__- 09:30 - 11:00 : Henning Basold (II)
__11:00 - 11:15 : break__- 11:15 - 12:15 : Neil Ghani (II)

# Talks

### Jurriaan Rot

**Title:** Companions and causal algebras

**Abstract:** The theory of coalgebras is a mathematical framework of various state-based systems and (infinite) data structures, parametric in an endofunctor B. It provides a categorical foundation for coinduction: the notion of a final B-coalgebra gives rise to coinductive definition and proof principles. In this talk I will introduce the notion of companion of a functor, a categorical generalisation of the lattice-theoretic notion of companion; the latter was proposed recently in the context of coinductive proof techniques. The companion is defined as a final object in a category of distributive laws, and generalises the final coalgebra. These distributive laws are often used in the theory of coalgebras to define operations on final coalgebras. I will show how a computation of the companion gives rise to a construction of causal operations (algebras) on final coalgebras such as streams (infinite sequences) and languages. This is based on joint work with Damien Pous. These causal algebras on streams form a special kind of sized types; in current work in progress (with Henning Basold), we are trying to extend the construction of causal algebras to more general sized types, which would provide a categorical foundation for those. If time permits, I will say a few words about this.

### Luigi Santocanale

**Title:**The aleph_1 continuous fragment of the modal mu-calculus

**Abstract:** For a regular cardinal κ, a formula of the modal µ-calculus is κ-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of κ-directed sets. We define the fragment Cℵ1(x) of the modal µ-calculus and prove that all the formulas in this fragment are ℵ1-continuous. For each formula φ(x) of the modal µ-calculus, we construct a formula ψ(x) ∈ Cℵ1(x) such that φ(x) is κ-continuous, for some κ, if and only if φ(x) is equivalent to ψ(x). Consequently, we prove that (i) the problem whether a formula is κ-continuous for some κ is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment Cℵ0(x) studied by Fontaine and the fragment Cℵ1(x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal µ-calculus. An ordinal α is the closure ordinal of a formula φ(x) if its interpretation on every model converges to its least fixed-point in at most α steps and if there is a model where the convergence occurs exactly in α steps. We prove that ω1, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0, 1, ω, ω1 by using the binary operator symbol + gives rise to a closure ordinal.

### Alexis Saurin

**Title:** Infinitary proof theory for linear logic with fixed points (from
straight to bouncing threads)

**Abstract:** Infinitary and circular proofs are commonly used in
fixed point logics. Being natural intermediate devices between
semantics and traditional finitary proof systems, they are commonly
found in completeness arguments, automated deduction, verification,
etc. However, their proof theory is surprisingly under-developed. In
particular, little is known about the computational behavior of such
proofs through cut elimination. Taking such aspects into account has
unlocked rich developments at the intersection of proof theory and
programming language theory. One would hope that extending this to
infinitary calculi would lead, e.g., to a better understanding of
recursion and corecursion in programming languages. Structural proof
theory is notably based on two fundamental properties of a proof
system: cut elimination and focalization. In this talk, we consider
the infinitary proof system μMALL∞ for multiplicative and additive
linear logic extended with least and greatest fixed points, and prove
these two key results. We thus establish μMALL∞ as a satisfying
computational proof system in itself, rather than just an intermediate
device in the study of finitary proof systems. In the last part of
the talk, we will discuss some ongoing work on relaxing the validity
condition for infinitary proofs and therefore accepting more
proofs. This is motivated by the fact that usual validity conditions
only consider straight threads -- progressing from conclusion to
premise. While natural in the cut-free setting, it is quite
restrictive in presence of cut This is joint work with Baelde, Doumane
and Jaber.

### Niccolo Veltri

**Title:** Partiality and container monads

**Abstract:** We investigate monads of partiality in Martin-Löf type
theory, following Moggi’s general monad-based method for modelling
effectful computations. These monads are often called lifting monads
and appear in category theory with different but related
definitions. In this paper we unveil the relation between containers
and lifting monads. We show that the lifting monads usually employed
in type theory can be specified in terms of containers. Moreover, we
give a precise characterization of containers whose extensions
carry a lifting monad structure. We show that these conditions are
tightly connected with Rosolini’s notion of dominance. We provide
several examples, giving particular emphasis on Capretta’s delay
monad and its quotiented variant.

### Valeria Vignudelli

**Title:** Environmental Bisimulations for Probabilistic Higher-Order Languages

**Abstract:**
The general topic of the talk are techniques for proving behavioural
equivalence in languages with both probabilistic and higher-order
operators. In particular, environmental bisimulations for probabilistic
higher-order languages are studied. In contrast with applicative
bisimulations, environmental bisimulations are known to be more robust and
do not require sophisticated techniques such as Howe’s in the proofs of
congruence.

As representative calculi, probabilistic call-by-name and call-by-value lambda-calculus, and a probabilistic (call-by-value) lambda-calculus extended with references (i.e., a store) are considered. In each case full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as ‘up-to techniques’, are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages.

This is a joint work with Davide Sangiorgi.