The seminar is joint between AlCo, Cosynus and Partout teams of LIX. To keep informed you can

Unless otherwise stated, all times below are in Paris local time.

Interactive Deep Reasoning

Pablo Donato (Ecole Polytechnique Paris)
Monday 30 May 2022 at 14:00, online seminar
Invited by the PARTOUT team.

In this talk, I will present the work I have been doing for my thesis in the past year and a half, which is an exploration in how to build formal proofs interactively through graphical, deep inference proof systems.

I will start with a demonstration of Actema, a prototype of graphical user interface for theorem proving in intuitionistic FOL based on direct manipulation of the proof state. A notable feature is the ability to reason by drag-and-dropping formulas within a sequent, which is a direct application of the subformula linking paradigm of K. Chaudhuri. The specificity of our approach lies in how we handle quantifiers through unification, as well as equalities. This enables both an elegant characterization, and a wide generalization of the behavior of standard rewrite tactics.

In the second part, I will present the “Bubble Calculus”, a new kind of nested sequent system which comes equipped with a nice graphical syntax. Inspired by the membranes of the Chemical Abstract Machine of Boudol and Berry, we add a so-called “bubble” construct for localizing interactions between propositions, which can be understood as internalizing the notion of premiss/subgoal inside judgments. By allowing bubbles to be polarized, one can then recover intuitionistic, dual-intuitionistic, bi-intuitionistic and classical logic as fragments which differ only in the allowed switch/membrane traversal rules.

In the third and last part, I will introduce an intuitionistic variant of the existential graphs of C. S. Peirce, arguably the first graphical proof system in the western logic tradition. To make the notation more readable, I will use a botanical metaphor where the graphs are represented as (nested) flowers. Contrarily to bubbles, flowers have a linear translation to and from traditional formulas, which allows to get completely rid of the latter in the proof system.

Willem Heijltjes

The Functional Machine Calculus

Willem Heijltjes (University of Bath)
Monday 23 May 2022 at 14:00, online seminar
Invited by the PARTOUT team.

I will present the Functional Machine Calculus (FMC), a simple model of higher-order computation with “reader/writer” effects: state, input/output, probabilities, and non-determinism. The main result is to extend two fundamental properties of the lambda-calculus to these effects: reduction in the FMC is confluent, and a system of simple types confers strong normalization.

The premise is to view the lambda-calculus as an instruction language for a simple stack machine, in the standard way of the Krivine machine, where application is “push” and abstraction is “pop”. The FMC then consists of two independent generalizations, that are natural from the perspective of the machine.

The first generalization, “locations”, is to allow multiple stacks (or streams) on the machine, each indicated by a “location”. Application and abstraction are parameterized in these locations, to give push and pop actions on the relevant stack. Then input streams, output streams, and memory cells are straightforwardly modelled by distinct locations.

The second generalization, “sequencing”, introduces sequential composition, following the perspective of terms as sequences of machine instructions, as well as a unit, the empty sequence. This is known from Hasegawa’s kappa-calculus and from concatenative programming languages, and enables the encoding of reduction strategies, including call-by-value lambda-calculus, and for the given effects, Moggi’s metalanguage, Levy’s call-by-push-value, and Haskell Arrows.

Reduction in the FMC is confluent, which is possible because encoded effect operations reduce algebraically, rather than operationally. It can be simply typed to confer strong normalization, and because effectful operations are fully typed, it has a semantics as a Cartesian closed category. Unlike in the monadic setting, reader/writer effects in the FMC combine seemlessly.

Joël Ouaknine

The Skolem Landscape

Joël Ouaknine (Max Planck Institute for Software Systems, Saarbrücken, Germany)
Thursday 19 May 2022 at 14:30, room Sophie Germain + online upon request (recording available)
Invited by the AlCo team.

The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, its decidability has been open for nearly a century! In this talk, I will present a survey of what is known on the Skolem Problem and related questions, including recent and ongoing developments.

Higher-order algebraic theories

Dylan McDermott (Reykjavik University)
Monday 9 May 2022 at 15:30, online seminar (slides available)
Invited by the Partout team.

First-order algebraic theories describe algebraic structures that can be presented by a collection of operators and equations. These were generalized by Fiore et al. to second-order algebraic theories, in which the operators can bind simple variables. Examples include lambda-abstraction in the untyped lambda-calculus, and quantification in first-order logic.

We generalize to higher-order theories, in which operators can bind variables of higher orders. I will discuss the resulting notion of nth-order algebraic theory, and some examples. Nth-order theories have a rich metatheory, in particular they have a universal characterization as a completion, under a class of colimits, of a freely generated category. It follows from this that there is a correspondence between (n+1)th-order algebraic theories and certain monads on nth-order algebraic theories, analogous to the correspondence between (monosorted) first-order theories and finitary monads on Set.

This is joint work with Nathanael Arkor.

Franck Djeumou

Neural Networks with Physics-Informed Architectures and Constraints for Dynamical Systems Modeling

Franck Djeumou (Department of Electrical and Computer Engineering at the University of Texas at Austin)
Thursday 14 April 2022 at 15:00, online seminar
Invited by the AlCo team.

Effective inclusion of physics-based knowledge into deep neural network models of dynamical systems can greatly improve data efficiency and generalization. Such a priori knowledge might arise from physical principles (e.g., conservation laws) or from the system’s design (e.g., the Jacobian matrix of a robot), even if large portions of the system dynamics remain unknown. We develop a framework to learn dynamics models from trajectory data while incorporating a priori system knowledge as inductive bias. By exploiting a priori system knowledge during training, the proposed approach learns to predict the system dynamics two orders of magnitude more accurately than a baseline approach that does not include prior knowledge, given the same training dataset.

Elena Ivanova

Efficient Synthesis of Controllers using Abstraction-Based Approaches

Elena Ivanova (Cosynus)
Wednesday 6 April 2022 at 14:00, room Grace Hopper
Invited by the Cosynus team.

The first part of the talk will be dedicated to a control synthesis for cyber-physical systems using abstraction-based control synthesis approaches. These approaches first create a finite-state abstraction (or a symbolic model) for a continuous or hybrid system and then refine the controller synthesized for the abstraction to a controller for the original system. Abstraction-based control synthesis techniques allow us to handle complex dynamics of CPS models and non-trivial specifications (for instance given by LTL formulas) but suffer from poor scalability. I will talk about how to improve the efficiency of ABS approaches when safety specification is considered. The second part of the talk will be dedicated to ongoing research on efficient approximations of the reachable sets.

Groupe fondamental et pavages du plan: quelques constructions

Léo Paviet Salomon (Greyc, Caen)
Thursday 24 March 2022 at 11:00, room Salle Henri Poincaré
Invited by the AlCo team.

On appelle sous-shift (ou sous-décalage) un ensemble de pavages ou de coloriages du plan respectant certaines contraintes locales. Historiquement introduits comme discrétisations de systèmes dynamiques continus, on se propose ici d’en étudier un invariant topologique, introduit par W.Geller et J.Propp, le Groupe Fondamental Projectif. A l’instar de la définition habituelle du groupe fondamental, un invariant d’espaces topologiques, il s’agira ici de comprendre comment l’on peut définir une notion de chemins dans les pavages, reliant les configurations entre elles, et d’étudier comment les déformations de ces chemins permettent d’associer à chaque pavage un unique objet algébrique: son groupe fondamental projectif. En particulier, on montrera dans cet exposé comment réaliser une large classe de groupes comme groupes fondamentaux de certains pavages.

Nathan Grosshans

Visibly pushdown languages in AC⁰

Nathan Grosshans (Universität Kassel, Germany.)
Thursday 17 March 2022 at 11:00, online seminar
Invited by the AlCo team.

One important research endeavour at the intersection of circuit complexity theory, algebraic automata theory and logic is the classification of regular languages according to their localisation within the internal structure of NC¹, the class of languages decided by Boolean circuits of polynomial size, logarithmic depth and with gates of constant fan-in. In some sense, the search for such a classification concentrates most of the open questions we have about the relationship between NC1 and its well-studied subclasses.

While many questions are still open, one of the greatest successes of this research endeavour has been the characterisation of the regular languages in AC⁰, the subclass of NC¹ corresponding to Boolean circuits of polynomial length, constant depth and with gates of unbounded fan-in. This characterisation takes the form of a triple languages-algebra-logic correspondence: a regular language is in AC0 if and only if its syntactic morphism is quasi-aperiodic if and only if it is definable in first-order logic over words with linear order and modular predicates.

It is natural to try to extend such results to classes of formal languages greater than the class of regular languages. A well studied and robust such class is given by visibly pushdown languages (VPLs): languages recognised by pushdown automata where the stack-height-behaviour only depends on the letters read from the input. Over the previous decade, a series of works concentrated on the fine complexity of VPLs, with several achievements: one of those was a characterisation of the class of visibly counter languages (basically VPLs recognised by visibly pushdown automata with only one stack symbol) in AC⁰ by Krebs, Lange and Ludwig. However, the characterisation of the VPLs in AC⁰ still remains open.

In this talk, I shall present a conjectural characterisation of the VPLs in AC⁰ obtained with Stefan Göller at the Universität Kassel. It is inspired by the conjectural characterisation given by Ludwig in his Ph.D. thesis as a generalisation of the characterisation for visibly counter languages, but that is actually false. In fact, we give a more precise general conjectural characterisation that builds upon recognisability by morphisms into Ext-algebras, an extension of recognisability by monoid-morphisms proposed by Czarnetzki, Krebs and Lange to suit the case of VPLs. This characterisation classifies the VPLs into three categories according to precise conditions on the Ext-algebra-morphisms that recognise them:

  • those that are TC⁰-hard;
  • those that are in AC⁰;
  • those that correspond to a well-identified class of “intermediate languages” that we believe to be neither in AC⁰ nor TC⁰-hard.
Paolo Pistone

On Equivalence and Similarity of Polymorphic Proofs and Programs

Paolo Pistone (University of Bologna)
Monday 7 March 2022 at 14:00, online seminar
Invited by the Partout team.

Under the proofs-as-programs paradigm, the problem of program equivalence, that is, of understanding whether two programs compute the same function, can be related to the problem of equivalence proof, that is, of understanding whether two formal derivations represent, in some sense, the same proof. In this talk I will discuss some methods to capture program/proof equivalence in System F, the paradigmatic language for parametric polymorphism, through the definition of an invariant, for each type, called the characteristic. This invariant provides a means to know whether, in the proofs of a given formula, propositional quantification (i.e. polymorphism) is eliminable via parametricity, yielding a way to test equivalence in a finite way. Moreover, I will sketch how parametricity and related methods for equivalence can be lifted to a more quantitative setting (as those arising from probabilistic or approximate computation) in which the vital property to understand is whether two programs, albeit non-equivalent, behave in a sufficiently similar way, so that replacing the one by the other cannot alter the results of computation too much.

Martin Krejca

The Power of Probabilistic Models in Optimization

Martin Krejca (LIP 6)
Thursday 17 February 2022 at 11:00, room Salle Philippe Flajolet
Invited by the AlCo team.

For many real-world optimization problems, the objective function is only indirectly accessible, for example, via simulations. In this setting, randomized search heuristics (RSHs) are applied to great success, guided solely by the quality of samples. One important class of these heuristics are estimation-of-distribution algorithms (EDAs), which maintain and refine a probabilistic model of the search space.

In this talk, I discuss some of my results on the theoretical analysis of EDAs by presenting properties of EDAs that set them apart from other RSHs. We see that EDAs cope inherently well with noisy objective functions, due to the probabilistic model tolerating faulty updates to a certain degree. However, we also show that these models typically degenerate if important updates are withheld for longer periods of time. We conclude by presenting how this problem is circumvented when applying better rules to handle updates.

Ulysse Chabaud

Holomorphic Quantum Computing

Ulysse Chabaud (Institute for Quantum Information and Matter, Caltech, US)
Thursday 3 February 2022 at 16:30, online seminar
Invited by the AlCo team.

The advent of quantum information processing promises dramatic advantages with respect to its classical counterpart, notably for computing. I will give an introduction to quantum computing through the lens of holomorphic functions, which allow us to elegantly describe both discrete- and continuous-variable quantum computations, using classical dynamical systems. As an application, I will discuss the characterisation of quantum properties that are necessary resources for quantum computational advantages, such as non-Gaussianity or entanglement.

Joint work with Saeed Merhaban (arXiv:2111.00117).

Variable binding and substitution for (nameless) dummies

Ambroise Lafont (UNSW Sydney)
Monday 25 October 2021 at 14:00, room Marcel-Paul Schützenberger (recording available)
Invited by the Partout team.

[Organizer’s note: this will be a hybrid seminar, simultaneously taking place at Salle Marcel-Paul Schützenberger and on BBB.]

By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

Joint work with Tom & Andre Hirschowitz, Marco Maggesi

Tarmo Uustalu

List monads

Tarmo Uustalu (Reykjavik University)
Monday 18 October 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.

We tend to speak of the (possibly empty) list monad and the nonempty list monad, meaning the free monoid monad and the free semigroup monad, as if those were the only monad structures on the list and nonempty list endofunctors (on Set). But they are not! It may at first seem hard to construct other list and nonempty list monads, but at a closer look it turns out that examples abound. There are infinitely many list monads with the singleton function as the unit that admit a presentation with one nullary and one binary operation, and infinitely many nonempty list monads with singleton as the unit and a presentation with one binary operation; some multiplications not only delete, but even duplicate and permute elements. There are list and nonempty list monads with singleton as the unit that have no finite presentation. There are nonempty list monads whose unit is the doubleton function. You cannot tell if a nonempty list monad presented to you as a blackbox is the free semigroup monad by testing the unit and multiplication on finitely many inputs. Etc. We are far from having classified all list monads or all nonempty list monads, but these are cool combinatorial problems.

This is joint work with Dylan McDermott and Maciej Piróg.

Constantin Enea

Towards Automated Verification of Concurrent or Distributed Software

Constantin Enea (Cosynus / LIX)
Tuesday 5 October 2021 at 14:00, room Philippe Flajolet
Invited by the Cosynus team.

I will talk about recent results concerning the problem of increasing the level of automation in formal verification of concurrent or distributed programs. These results span various approaches from testing, finite state model-checking, to SMT-based proofs. Also, they apply to various classes of programs from concurrent data types, to distributed databases, or applications thereof.

Christian Johansen

History-aware Higher Dimensional Modal Logic

Christian Johansen (Norwegian University of Science and Technology)
Wednesday 7 July 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

This talk presents a modal logic over HDAs which incorporates two modalities for reasoning about “during” and “after”. This higher dimensional modal logic (HDML) is decidable and an “almost” complete axiomatic system exists for it. When the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. One can isolate the class of HDAs that encode Mazurkiewicz traces and show how HDML, with natural definitions of corresponding Until operators, can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces) or the branching time ISTL. A preliminary study of the expressiveness of the basic HDML language wrt. bisimulations has concluded that HDML captures the split-bisimulation. One can also add backward-looking modalities (i.e., past modalities) so to increase the expressiveness so to be able to capture the hereditary history-preserving bisimulation. Classical examples from the literature that are used to distinguish one-or-another bisimulation can be distinguished in this hHDML using a specially crafted formula. I will show these interesting examples and talk about the respective literature, if time permits.

Sven Dziadek

Greibach Normal Form and Simple Automata for Weighted ω-Context-Free Languages

Sven Dziadek (Universität Leipzig)
Wednesday 30 June 2021 at 11:00, online seminar
Invited by the Cosynus team.

In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of ω-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted context-free languages, or ω-algebraic series, can be represented as solutions of (mixed) ω-algebraic systems of equations and by weighted ω-pushdown automata.

In our first main result, we show that (mixed) ω-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple ω-reset pushdown automata recognize all ω-algebraic series. Simple ω-reset automata do not use ε-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted context-free languages.

This talk is based on this article and its corresponding short version.

Sonia Vanier

Distributed Denial of Service cyber-attacks in 5G networks: a robust approximation approach

Sonia Vanier (Délégation au LIX, et Université Paris, Panthéon-Sorbonne)
Thursday 24 June 2021 at 14:30, online seminar
Invited by the AlCo team.

Distributed Denial of Service (DDoS) cyberattacks represent a major security risk for network operators and internet service providers. They thus need to invest in security solutions to protect their network against DDoS attacks. The present work focuses on deploying a network function virtualization based architecture to secure a network against an on-going DDoS attack. We assume that the target, sources and volume of the attack have been identified. However, due e.g. to 5G network slicing, the exact routing of the illegitimate flow in the network is not known by the internet service provider. We seek to determine the optimal number and locations of virtual network functions in order to remove all the illegitimate traffic while minimizing the total cost of the activated virtual network functions. We propose a robust optimization framework to solve this problem. The uncertain input parameters correspond to the amount of illegitimate flow on each path connecting an attack source to the target and can take values within a predefined uncertainty set. In order to solve this robust optimization problem, we develop an adversarial approach in which the adversarial sub-problem is solved by a Branch & Price algorithm. The results of our computational experiments, carried out on medium-size randomly generated instances, show that the proposed solution approach is able to provide optimal solutions within short computation times

Alex Kavvos

Client-Server Sessions in Linear Logic

Alex Kavvos (Bristol)
Wednesday 23 June 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.

We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of weakening and contraction. This makes them a suitable logical device for encapsulating the pattern of a server receiving requests from an arbitrary number of clients on a single channel. Guided by this intuition we formulate a system of session types based on Classical Linear Logic with coexponentials, which is suited to modelling client-server interactions. We also present a session-typed functional programming language for client-server programming, which we translate to our system of coexponentials.

Krzysztof Ziemiański

Tracks in Higher Dimensional Automata

Krzysztof Ziemiański (University of Warsaw)
Wednesday 23 June 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

The main goal of my talk is to present two models of executions of Higher Dimensional Automata. A track in a HDA is a sequence of cells such that every cell is either an upper face or an upper coface of the preceding one. To every track we can assign the (evi)pomset of its events; it is a labeled interval order equipped with an additional secondary ordering. Then we consider the set of tracks between fixed source and target cells, up to certain equivalence. This set is naturally a presheaf over the category of evipomsets, which is our first model of executions of HDA. This model can be simplified. When we restrict to step-sequence executions, ie, tracks in which the consecutive cells have only one common vertex, we obtain a presheaf over permutahedral category. This model is combinatorially simpler. At first glance it seems too restrictive but there is some evidence that this is not the case: the space of topological executions is homotopy equivalent to the geometric realization of the permutahedral model.

Federico Olimpieri

Intersection type distributors

Federico Olimpieri (LIPN)
Monday 7 June 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.

We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

Francesco Gavazzo

On Monadic Rewriting Systems

Francesco Gavazzo (University of Bologna)
Wednesday 19 May 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

Motivated by the study of effectful programming languages and computations, I will introduce the theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, effects being modelled as monads. Such systems are to effectful computations and programming languages what traditional rewriting systems are to pure computations and programming languages. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining mathematically and operationally meaningful notions of monadic rewriting turns out to be simply not possible for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible.

I will answer that question by showing that the so-called weakly cartesian monads precisely describe computational effects for which monadic rewriting is well-behaved. If monads are given as equational theories, as it is in the case of algebraic effects, a sufficient condition ensuring monadic rewriting to be well-behaved can be given by looking at the shape of the theory only: such a condition dates back to an old theory by Guatam and requires equations to be linear. Finally, I will apply the abstract theory of monadic rewriting systems to the call-by-value λ-calculus with algebraic effects, this way obtaining the extension of the well-known confluence and standardisation theorems to an effectful setting.

Analog characterization of standard complexity classes by means of ODEs

Riccardo Gozzi (Instituto Superior Técnico, Portugal)
Wednesday 12 May 2021 at 10:30, online seminar
Invited by the AlCo team.

In this presentation it will be shown how to make use of ordinary differential equations (ODEs) to describe standard complexity classes. Previously it was shown that the classes P and FP can be characterized with ODEs. Here we show that ODEs can also be used to characterize a wide range of computable functions, from exponentials up to including all elementary functions. It will be also discussed the case of space complexity classes, introducing the definition of a particular dynamical system able to describe functions in FPSPACE. Finally, to complement what have been done with functions, the treatment of classes of languages such as EXPTIME and PSPACE will be included in the analysis.

Georg Struth

Verifying Hybrid Systems with Interactive Theorem Provers

Georg Struth (University of Sheffield)
Wednesday 21 April 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

Hybrid systems integrate continuous dynamics and discrete control. A prominent approach is differential dynamic logic (dL), a modal logic for reasoning about ordinary differential equations and their solutions within hybrid programs. Over the last decade, a domain-specific sequent calculus for dL has been developed together with an intricate explicit substitution calculus for it. It has been integrated into the KeYmaera X tool and proved its worth in numerous case studies.

This talk presents an algebraic reconstruction of this approach and the first verification and refinement components in an interactive proof assistant inspired by it. Our components are based on shallow embeddings in which the proof theory of dL is by and large replaced by semantic equational reasoning about orbits and trajectories of dynamical systems in combination with discrete state updates. We use algebras, in particular variants of Kleene algebras and predicate transformer algebras, for automatic verification condition generation. We currently support a component for reasoning with weakest liberal preconditions, a Hoare logic and a refinement calculus for hybrid programs.

These allow us to verify hybrid programs in various ways: starting from hybrid program specifications based on ordinary differential equations, we can certify solutions of locally Lipschitz-continuous vector fields using the Picard-Lindelöf theorem and then reason explicitly about them. Alternatively we can represent solutions of continuous vector fields implicitly by invariant sets. Finally, we can analyse hybrid program that specify trajectories or orbits of hybrid systems directly.

Apart from presenting the algebras used and their extension and instantiation to hybrid program semantics, I will present some examples, comment on the intricacies of formalising the approach within the Isabelle/HOL proof assistant, and outline some future directions for this line of work, time permitting.

This work is joint with Jonathan Julián Huerta y Munive, and partially funded by CONACYT.

Renaud Vilmart

An introduction to ZX-calculus

Renaud Vilmart (LMF, ENS Paris-Saclay)
Wednesday 14 April 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

The ZX-Calculus is a powerful graphical language for representing quantum processes, stemming from category theory. Its primitives are close to that of the hardware these processes will supposedly be implemented on, and yet it enjoys some level of abstraction. In particular, it is equipped with an intuitive equational theory, allowing us to relate processes that are equivalent, i.e. that represent the same quantum evolution. The plasticity and the equational theory of the language make it a particularly good candidate for unifying different models of quantum computation, for optimisation, as well as for verifying properties or equivalences of processes.

Janna Burman

Time-Optimal Self-Stabilizing Leader Election in Population Protocols

Janna Burman (LISN, Université Paris-Saclay)
Thursday 8 April 2021 at 14:30, online seminar
Invited by the AlCo team.

We consider the standard population protocol model, where (a priori) indistinguishable and anonymous agents interact in pairs according to uniformly random scheduling. The self-stabilizing leader election problem requires the protocol to converge on a single leader agent from any possible initial configuration. We initiate the study of time complexity of population protocols solving this problem in its original setting: with probability 1, in a complete communication graph. The only previously known protocol by Cai, Izumi, and Wada [Theor. Comput. Syst. 50] runs in expected parallel time Θ(n²) and has the optimal number of n states in a population of n agents. The existing protocol has the additional property that it becomes silent, i.e., the agents’ states eventually stop changing.

Observing that any silent protocol solving self-stabilizing leader election requires Ω(n) expected parallel time, we introduce a silent protocol that uses optimal O(n) parallel time and states. Without any silence constraints, we show that it is possible to solve self-stabilizing leader election in asymptotically optimal expected parallel time of O(log n), but using at least exponential states (a quasi-polynomial number of bits). All of our protocols (and also that of Cai et al.) work by solving the more difficult ranking problem: assigning agents the ranks 1, … ,n.

Benoit Monin

Une petite histoire de la K-trivialité

Benoit Monin (Université de Créteil)
Thursday 1 April 2021 at 14:30, online seminar
Invited by the AlCo team.

La complexité de Kolmogorov est utilisée avec succès pour caractériser l’aléatoire pour les chaînes binaires infinies : Il s’agit des chaînes dont la complexité de Kolmogorov de leurs préfixes est maximale. A l’opposé, les chaînes binaires infinies dites “K-triviales” sont celles dont la complexité de Kolmogorov de leurs préfixes est minimale. La classe des K-triviaux est dénombrable, et contient “juste un peu plus” que les chaînes binaires infinies calculables. Les nombreuses études sur les K-triviaux depuis une vingtaine d’années ont révélé la grande richesse de cette classe. Nous en présenterons les différents aspects.

Arnaud Spiwack

Linear Constraints

Arnaud Spiwack (Tweag)
Wednesday 31 March 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.

In the past few years, I’ve been involved in extending the type system of the Haskell programming language to support linear types. In one sentence, a linear argument must be consumed exactly once in the body of its function; a linear function is a function whose argument is linear. Such a linear type system comes from linear logic (or, in this particular case, intuitionistic linear logic, but who’s counting?) seen through the lens of the Curry-Howard correspondence. Linear typing has two main families of applications: making pure interface to mutable data structures, such as arrays (“pure” means that functions are functions in the sense of mathematics); and enforcing protocol in the type level, for instance making sure file handles are eventually closed and not written to after being closed. An example that combines both aspects is safe manual memory management, much in the style that the Rust programming language allows.

This is all possible in the, latest, 9.0 release of GHC. However these applications, using GHC 9.0’s linear types require quite a bit of additional syntactic bureaucracy, compared to their unsafe equivalent. In this talk, after introducing Haskell’s linear types, I’ll present linear constraints, a front-end feature for linear typing that decreases the bureaucracy of working with linear types. Linear constraints are implicit linear arguments that are to be filled in automatically by the compiler. Linear constraints are presented as a qualified type system, together with an inference algorithm which extends OutsideIn, GHC’s existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell.

Giuseppe Di Molfetta

Gauge-invariance in celullar automata and multi-scales analysis

Giuseppe Di Molfetta (Aix-Marseille University)
Thursday 18 March 2021 at 14:30, online seminar
Invited by the AlCo team.

Cellular Automata constitute the most established distributed model of computation on space-time grid. It is clearly physics-like, in the sense that it shares some fundamental symmetries such as homogeneity (invariance of the physical laws in time and space), causality, and often reversibility. When a CA is invariant under a transformation identically performed at every point of the configuration space, they are said to have a global symmetry. Typical global symmetries include reflections, rotations, time inversion. Local symmetries, the cornerstone of gauge theories, is a stronger constraint. I will provide a constructive method, a step-by-step procedure, to make cellular automata invariant under the local action of a gauge group and the notion of gauge-equivalence will be formalized. Then, I will extend such results into the Quantum realm by means of a concrete example. In conclusion, I will discuss how such discrete time and discrete space gauge invariant automata can be described at larger scale, e.g. by differential equations, with and without information loss.

Niccolò Veltri

Proof Theory of Skew Monoidal Categories

Niccolò Veltri (Tallinn University of Technology)
Monday 15 March 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.

(Joint work with Tarmo Uustalu and Noam Zeilberger)

The skew monoidal categories of Szlachányi are a weakening of monoidal categories where the three structural laws of left and right unitality and associativity are not required to be isomorphisms but merely transformations in a particular direction. In this talk, we show that the free skew monoidal category on a set of generating objects can be concretely presented as a sequent calculus. This calculus enjoys cut elimination and admits focusing, i.e. a subsystem of canonical derivations, which solves the coherence problem for skew monoidal categories.

We also develop sequent calculi for partially normal skew monoidal categories, which are skew monoidal categories with one or more structural laws invertible. Each normality condition leads to additional inference rules and equations on them. We prove cut elimination and we show that the calculi admit focusing. The result is a family of sequent calculi between those of skew monoidal categories and (fully normal) monoidal categories. On the level of derivability, these define 8 weakenings of the (unit,tensor) fragment of intuitionistic non-commutative linear logic.

If time allows it, we briefly discuss the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew closed categories in turn are a weakening of the closed categories of Eilenberg and Kelly where no structural law is required to be invertible and the presence of a monoidal structure is not required.

Constantin Enea

Automated Formal Testing of Transactional Databases and Applications

Constantin Enea (IRIF)
Wednesday 10 March 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and are resilient to failures. Modern databases provide different isolation levels for transactions corresponding to different tradeoffs between consistency and availability. The weaker the isolation level, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors.

I will present a series of recent results that concern the problem of testing transactional databases and database-backed applications. First, I will focus on the problem of checking whether a given execution of a transactional database adheres to some isolation level, showing that isolation levels like read committed, read atomic, and causal consistency are polynomial-time checkable while prefix consistency and snapshot isolation are NP-complete in general. These results complement a previous NP-completeness result concerning serializability. Moreover, in the context of NP-complete isolation levels, we devise algorithms that are polynomial time assuming that certain parameters in the input executions, e.g., the number of sessions, are fixed. Second, I will present MonkeyDB, a mock storage system for testing database-backed applications. MonkeyDB supports a Key-Value interface as well as SQL queries under multiple isolation levels. It uses a logical specification of the isolation level to compute, on a read operation, the set of all possible return values. MonkeyDB then returns a value randomly from this set. We show that MonkeyDB provides good coverage of weak behaviors, which is complete in the limit.

Giulio Guerrieri

Understanding the lambda-calculus via linearity and rewriting.

Giulio Guerrieri (University of Bath)
Monday 1 March 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.

The lambda-calculus is the model of computation underlying functional programming languages and proof assistants. Actually, there are many lambda-calculi, depending on the evaluation mechanism (e.g., call-by-name, call-by-value, call-by-need) and computational feature that the calculus aims to model (e.g., plain functional, non-deterministic, probabilistic, infinitary).

The existence of different paradigms is troubling because one apparently needs to study the theory and semantics of each one separately.

We propose a unifying meta-theory of lambda-calculi, where the study is rooted on a unique core language, the bang calculus, a variant of the lambda-calculus inspired by linear logic: a bang operator marks which resources can be duplicated or discarded.

The bang calculus subsumes both call-by-name and call-by-value. A property studied in the bang calculus is automatically translated in the corresponding property for the call-by-name lambda-calculus and the call-by-value lambda-calculus, thanks to two different embeddings of the lambda-calculus in the bang calculus. These embeddings are grounded on a proof theory: they are an adaptation of Girard’s two translations of intuitionistic logic into linear logic.

Advanced computational features are usually obtained by adding new operators to a core language. Instead of studying the operational properties of the extended language from scratch, we propose a simple method to study them modularly: if an operational property holds in the core language and in the new operators separately, then a simple test of good interaction between core language and new operators guarantees that the property lifts to the whole extended language. This approach is first developed in abstract rewriting systems.

Ambroise Lafont

Mathematical specifications of programming languages via modules over monads

Ambroise Lafont (UNSW Sydney)
Monday 22 February 2021 at 10:30, online seminar (recording available)
Invited by the Partout team.

Research in the field of programming languages traditionally relies on a definition of syntax modulo renaming of bound variables, with its associated operational semantics. We are interested in mathematical tools allowing us to automatically generate syntax and semantics from basic data. We pay particular attention to the notion of substitution, using the categorical notions of monads and modules over them. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets. We provide a further notion of transition monads which takes into account the operational semantics. We give examples of specifications for transition monads, in the spirit of Initial Semantics, where an object is characterized by some initiality property in a suitable category of models.

Miki Hermann

Logical Analysis of Data

Miki Hermann (LIX)
Thursday 18 February 2021 at 14:30, online seminar
Invited by the AlCo team.

We show how to cope with Big Data by means of Automated Deduction. We generate a Horn or a bijunctive formula from sets of positive and negative tuples T and F, respectively These sets of tuples have been previously shortened to a locally minimal length, provided that the two sets T and F keep an empty intersection. Since the problem to find the minimal length is an NP-optimization problem, we apply different approximation strategies. We also apply two approaches to formula production: (1) the LARGE approach, where only tuples of F falsify the produced formula, and (2) EXACT, where only tuples of T satisfy the formula. In case of the large approach we apply a set cover approximation algorithm to keep the minimal set of clauses falsifying all tuples from the set F. The produced formula can be used to further characterize subsequent sets of tuples and identify their membership among the true or false examples. The whole system, called MCP for Multiple Characterization Problem, has been implemented and can be found at

(research done in collaboration with Gernot Salzer, Technische Universität Wien, Vienna, Austria)

Uli Fahrenberg

Generating Posets Beyond N

Uli Fahrenberg (LIX)
Wednesday 17 February 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

We introduce iposets - posets with interfaces - equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem more interesting for modeling concurrent and distributed systems, can be generated, but not all posets. Generating posets is also important for constructing free algebras for concurrent semirings and Kleene algebras that allow compositional reasoning about such systems.

Daniel Murfet

Gentzen-Mints-Zucker duality: sequent calculus vs λ-calculus

Daniel Murfet (University of Melbourne)
Monday 8 February 2021 at 09:30, online seminar
Invited by the Partout team.

I will report on joint work with Will Troiani, in which we revisit Howard’s work on the Curry-Howard correspondence and interpret it as an isomorphism between a category of proofs in intuitionistic sequent calculus and a category of terms in simply-typed λ-calculus. Some version of this is known to the experts due to work of Mints, Zucker and others, but not for Gentzen’s original calculus. I will explain our technical contributions to the understanding of normal forms of sequent calculus proofs, and our view that the fundamental duality expressed is not between “proofs and programs” but between local and global presentations of a logico-computational structure.

Matteo Acclavio

Games for constructive modal logics

Matteo Acclavio (University of Luxembourg)
Monday 1 February 2021 at 14:00, online seminar
Invited by the Partout team.

Constructive modal logics are extensions of intuitionistic propositional logic with certain modal axioms. Many proof systems are known for these logics, but the only available denotational semantics is defined by means of an abstract construction, based on the quotient of their lambda terms.

The general aim of our work is to define a game semantics for constructive modal logics. In this talk I will define the winning strategies for a formula and show the correspondence between winning strategies and proofs. I will show how winning strategies can be defined as the projection of specific paths in a graphical proof system defined for this purpose - combinatorial proofs.

(this talk is based on a joint work with Davide Catta and Lutz Strassburger)

Robin Piedeleu

A diagrammatic axiomatisation of finite-state automata

Robin Piedeleu (University College London)
Wednesday 27 January 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

In this talk I will present a fully diagrammatic approach to the theory of finite-state automata, based on reinterpreting their usual state-transition graphs as string diagrams. Moreover, I will give an equational theory that completely axiomatises language equivalence in this new setting. The proposed axiomatisation is finitary— a result which is provably impossible to obtain for the usual one-dimensional syntax of regular expressions.

Abstract rewriting Internalised

Maxime Lucas (Université Sorbonne Paris Nord)
Wednesday 13 January 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.

There are two historical trends in rewriting theory: “abstract rewriting”, where one rewrites terms, and “algebraic rewriting”, where one rewrites linear combinations of terms. Although the two theories enjoy similar results, there are subtle differences that prevent the development of a unified theory: for example in algebraic rewriting any reflexive relation is both symmetric and transitive. In this talk we present a generic framework to study rewriting in a category C satisfying some suitable hypothesis. In the case C = Set we recover abstract rewriting, while algebraic rewriting corresponds to the case where C is the category of vector spaces. In this framework, we express notions of termination, confluence and local confluence using a notion of rewriting strategy, and prove an analogue of Newman’s Lemma. Finally, we hint at the higher dimensional analogue of this framework, with a view towards homotopy.