This page


  • The workshop will start on Monday, July 3 2017 at 10:00am with coffee and viennoiseries. Talks will start at 10:30.
  • Otherwise, the session times will be 9:00-12:15 and 14:00-17:30.
  • The talks will take place in Amphitheatre Revard (in red on the map).
  • Contributed talks may last up to 1h, including questions.

Monday, July 3

Tuesday, July 4

Wednesday, July 5

Thursday, July 6


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.