# Seminar

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.

## Monadic rewriting systems and the word problem

Carl-Fredrik Nyberg Brodda (Université Gustave Eiffel)
Wednesday 5 April 2023 at 14:00, room TBA
Invited by the PARTOUT team.

The word problem for finitely presented groups and semigroups is one of the most fundamental problem in all combinatorial algebra. Language-theoretic methods can be used to study it, which has revealed deeps links in group theory between accessible groups, virtually free groups, the geometry of context-free graphs, and context-free languages. In this talk, I will go over some recent progress on how I have developed these methods and results to semigroup theory, as well as new techniques I developed in order to reduce such problems to problems about groups. This includes results from the theory of string rewriting systems, and a non-constructive – but highly algebraic – definition of the class of all context-free languages (or indeed the class of ET0L languages, indexed languages, etc.) via monadic rewriting systems.

## Polarized Linear Logic with Fixpoints

Farzad Jafarrahmani (Laboratoire d'Informatique de Paris 6 (LIP6))
Wednesday 29 March 2023 at 14:00, room Philippe Flageolet
Invited by the PARTOUT team.

In this talk, I will present a joint work with Thomas Ehrhard and Alexis Saurin on μLLP, which can be viewed both as an extension of Laurent’s Polarized Linear Logic, LLP, with least and greatest fixpoints, and as a polarized version of Baelde and Miller’s Linear Logic with fixpoints (μMALL and μLL). We take advantage of the implicit structural rules of μLLP to introduce a term syntax for this language, in the spirit of the classical lambda-calculus and of system L in the style of Curien, Herbelin and Munch-Maccagnoni. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on the notion of non-uniform totality spaces and the notion of categorical model for linear logic with fixpoint. At the end, I will show you an adequacy result for μLLP between these operational and denotational semantics, from which we derive a normalization property for μLLP thanks to the properties of the totality interpretation.

## On the External Validity of Average-Case Analyses of Graph Algorithms

Philipp Fischbeck (Hasso Plattner Institute, University of Potsdam)
Thursday 16 March 2023 at 10:30, room Salle Emmy Noether
Invited by the ALCO team.

The number one criticism of average-case analysis is that we do not actually know the probability distribution of real-world inputs. Thus, analyzing an algorithm on some random model has no implications for practical performance. At its core, this criticism doubts the existence of external validity, i.e., it assumes that algorithmic behavior on the somewhat simple and clean models does not translate beyond the models to practical performance real-world input. With this paper, we provide a first step towards studying the question of external validity systematically. To this end, we evaluate the performance of six graph algorithms on a collection of 2745 sparse real-world networks depending on two properties; the heterogeneity (variance in the degree distribution) and locality (tendency of edges to connect vertices that are already close). We compare this with the performance on generated networks with varying locality and heterogeneity. We find that the performance in the idealized setting of network models translates surprisingly well to real-world networks. Moreover, heterogeneity and locality appear to be the core properties impacting the performance of many graph algorithms.

## Perfect matchings, quantum computing and monoidal categories

Titouan Carette (University of Latvia)
Thursday 9 March 2023 at 10:30, room Salle Grace Hopper
Invited by the ALCO team.

In 2002, Leslie Valiant designed a computational model based on counting the number of perfect matchings of weighted graphs: the matchgates. Matchgates can directly be interpreted as quantum processes providing an original combinatorial approach to quantum computing. In the general case, counting perfect matchings is #P-complete. However, in the specific case of planar graphs, the FKT-algorithm allows counting perfect matchings in polynomial time. As a consequence, planar matchgates provide a class of quantum computation that can be classically simulated in polynomial time.Completely independently, in 2010, as a part of the categorical quantum mechanics program, Coecke and Kissinger introduced the ZW-calculus, a graphical language inspired by two kinds of entanglement, the GHZ-states and W-states. This calculus quickly demonstrated interesting algebraic properties allowing it to be the first graphical language to be proven universal and complete for all linear maps. In this talk, I will present joint works with Étienne Moutot, Thomas Perez and Renaud Vilmart, building a bridge between the two formalisms: matchgates and ZW-calculus. It appears that reformulating matchgate theory into the category-theoretic framework of ZW-calculus allows for a much simpler presentation. Conversely, the matchgate approach provides the ZW-calculus with a straightforward combinatorial interpretation. I will introduce a fragment of ZW-calculus, the planar W-calculus, and show that it is universal and complete for matchgates. Then I will present a variety of consequences, from new algorithms for perfect matching counting and quantum simulation to a diagrammatical approach to determinant theory.

## Generic pattern unification: a categorical approach

Ambroise Lafont (Cambridge)
Monday 9 January 2023 at 14:00, online seminar
Invited by the PARTOUT team.

We provide a generic categorical setting for Miller’s pattern unification. The syntax with metavariables is generated by a free monad applied to finite coproducts of representable functors; the most general unifier is computed as a coequaliser in the associated multisorted Lawvere theory. Our setting handles simply-typed second-order syntax, linear syntax, or (intrinsic) polymorphic syntax such as system F.

## Two-Dimensional Drift Analysis: Optimizing Two Functions Simultaneously Can Be Hard

Duri Andrea Janett (LIX)
Thursday 5 January 2023 at 11:00, room Salle Philippe Flajolet
Invited by the ALCO team.

The performance of Evolutionary Algorithms (EAs) in dynamic environments, that is, environments in which the fitness function changes over time, has recently been studied (e.g., [Lengler, Meier, 2020]). In this talk, we develop and analyse a minimal example TwoLinear of a dynamic environment that can be hard for EAs. The environment consists of two linear functions f1 and f2 with positive weights 1 and n, and in each generation selection is based on one of them at random. They only differ in the set of positions that have weight 1 and n. We show that the (1+1)-EA with mutation rate χ/n is efficient for small χ on TwoLinear, but does not find the shared optimum in polynomial time for large χ.To obtain the above result, we apply drift analysis in two dimensions. Drift analysis is one of the most powerful techniques to analyse the performance and behaviour of EAs. Previously, it has only been applied in one dimension. Here, we are in the case of two random variables X1, X2, and the drift is approximatively given by A·(X1, X2)T for a matrix A. More precisely, we are in the case where X1 and X2 impede each other’s progress, and we give a full characterisation of this case.

## A positive perspective on term representation

Dale Miller (LIX)
Monday 5 December 2022 at 14:00, online seminar
Invited by the PARTOUT team.

Structural proof theory provides principles for organizing syntax. Many researchers have used the theory of proofs developed by Gentzen and Prawitz to design both the representation of and operations on terms. In this talk, we illustrate this tight connection between proofs and terms by using the structure of proofs in the focused proof system LJF to design term structures. Since the proof theory of LJF does not determine a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible. Such a representation of terms provides an explicit method for sharing term structures. In this setting, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to encoding untyped lambda-terms. We also exploit concurrency theory techniques—traces and simulation—to compare untyped lambda-terms using different structuring disciplines. [This is joint work with Jui-Hsuan Wu and is based on a paper that will appear in CSL 2023.]

## Reasonable Space and the Lambda Calculus

Beniamino Accattoli (LIX)
Monday 28 November 2022 at 14:00, online seminar
Invited by the PARTOUT team.

The lambda calculus is an expressive mathematical formalism that elegantly captures the core of functional programming languages. The evaluation of programs is modeled as a symbolic rewriting system far from low-level implementative details. This aspect has the drawback that it is not clear how to measure the time and space complexity of functional programs in a reasonable way, that is, in a way that agrees with standard computational complexity. The talk focuses on reasonable space for the lambda calculus, about which—until very recently—almost nothing was known. The talk shall survey recent results in collaboration with Ugo Dal Lago and Gabriele Vanoni (appeared in POPL 2021, LICS 2021, LICS 2022, and ICFP 2022) which have clarified the topic, and led to the first reasonable space cost model for the lambda calculus able to account for logarithmic space.

## Copying and Movement, in Substructural Logics, for Natural Language Reasoning

Monday 21 November 2022 at 14:00, online seminar
Invited by the PARTOUT team.

In 1958 Lambek proposed the logic of a residuated monoid to reason about syntax of natural language. This logic was amongst the first substructural logics. It did not have contraction or weakening, properties that indeed were not necessary for fixed word order languages. As a result of these, Lambek’s logic could not reason about free word order languages, e.g. as in Sanskrit and Latin, and discourse structure, e.g. as in “John slept. He snored.” In this talk, I will show how endowing the logic with controlled modalities solves the problem. I will go through the syntax and semantics of the logic and establish applications to natural language. This is joint work with Lachlan McPheat, Hadi Wazni and Ian Lo Kin.

## Bell numbers in Matsunaga's and Arima's Genjikō combinatorics: Modern perspectives and local limit theorems

Hsien-Kuei Hwang (LIX)
Wednesday 9 November 2022 at 11:00, room Grace Hopper
Invited by the Alco team.

We examine and clarify in detail the contributions of Yoshisuke Matsunaga (1694?–1744) to the computation of Bell numbers in the eighteenth century (in the Edo period), providing modern perspectives to some unknown materials that are by far the earliest in the history of Bell numbers. Later clarification and developments by Yoriyuki Arima (1714–1783), and several new results such as the asymptotic distributions (notably the corresponding local limit theorems) of a few closely related sequences are also given.

## Looking inside the modalities: subatomic proof theory for modal logics

Marianela Morales (LIX)
Monday 7 November 2022 at 14:00, online seminar
Invited by the PARTOUT team.

There are many different cut-elimination techniques in the deep inference literature, exploiting different aspects of the proof systems they work on. A particular methodology does however stand out for its generality: cut-elimination via splitting. Even though this proof has to be redone for every proof system anew, there is a certain repeating pattern. In order to formalize this pattern and to obtain a general cut-elimination method that works for many proof systems at the same time, the method of subatomic proof theory has been developed. The basic idea is to treat atoms as binary connectives, leading to a uniform shape of all inference rules. In our work in progress we extend this idea to classical modal logics. This means that also the unary modalities are treated like binary connectives. We show soundness and completeness of the subatomic system, and we show cut-elimination via splitting for the linear fragment of the system.

## Distributing and trusting proof checking

Farah Al Wardani (LIX)
Monday 24 October 2022 at 14:00, online seminar
Invited by the PARTOUT team.

When a proof-checking kernel completes the checking of a formal proof, that kernel asserts that a specific formula follows from a collection of lemmas within a given logic. We describe a framework in which such an assertion can be made globally so that any other proof assistant willing to trust that kernel can use that assertion without rechecking (or even understanding) the formal proof associated with that assertion. In this framework, we propose to move beyond autarkic proof checkers—i.e., self-sufficient provers that trust proofs only when they are checked by their kernel—to an explicitly non-autarkic setting. This framework must, of course, explicitly track which agents (proof checkers and their operators) are being trusted when a trusting proof checker makes its assertions. We describe how we have integrated this framework into a particular theorem prover while making minor changes to how the prover inputs and outputs text files. This framework has been implemented using off-the-shelf web-based technologies, such as JSON, IPFS, IPLD, and public key cryptography.

## Verification of cyber-physical systems: a counterexample-guided approach

Guillaume Berger (LIX)
Thursday 20 October 2022 at 09:00, room Henri Poincaré
Invited by the Cosynus team.

We study counterexample-guided methods to compute stability and safety certificates for hybrid linear systems. Counterexample-guided methods involve interactions between a learner that produces candidate certificates and an oracle that verifies whether a given candidate certificate is valid. We consider two templates of polyhedral certificates: a fixed-complexity and an adaptive-complexity template. In the fixed-complexity template, the number of linear pieces of the certificate is fixed; while in the adaptive-complexity template, the number of linear pieces is updated during the learning process. For both approaches, we discuss the advantages and disadvantages, and we provide algorithmic frameworks for the computation of a certificate. Finally, we discuss current work involving extensions to correct-by-design controller synthesis.Guillaume Berger is a postdoctoral researcher in the Programming Language Verification (PLV) lab at CU Boulder, in the team of Sriram Sankaranarayanan. He received his PhD. in Mathematical Engineering from UCLouvain, Belgium, in 2021. His research focuses on automatic techniques for verification and design of complex modern systems, like cyber-physical systems, networked systems and hybrid systems.

## Totalization of Ordinary Differential Equations

Riccardo Gozzi (LIX)
Wednesday 19 October 2022 at 11:00, room Grace Hopper
Invited by the AlCo team.

“The totalization process was introduced by Denjoy in 1912 as an interative procedure to obtain the antiderivative of any derivative. This idea has generated the notion of Denjoy integral, first of a serie of notions of integration proposed in literature as alternatives to Riemann and Lebesgue integrals in order to successfully retrieve the antiderivative of some class of pathological derivatives. This talk follows the path taken by Denjoy, describing the details of its solution for the problem of integration, and applies it to the realm of first order ODEs, exploring the set theoretical complexity of obtaining the solution of the dynamical system for ODEs with specific pathological right-hand terms.”

## A type theory for formal category theory

Max S. New (University of Michigan (MPLSE))
Monday 17 October 2022 at 14:00, online seminar
Invited by the PARTOUT team.

We present a type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. By restricting the type theory to an ordered linear variant of predicate logic, we guarantee that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proof necessary. Important category theoretic proofs such as the Yoneda lemma become simple type theoretic proofs about the relationship between unit, tensor and function types, and can be seen to be ordered refinements of familiar theorems in predicate logic. The type theory comes with a sound and complete notion of categorical model based on virtual equipments, a known setting for formal category theory that has been shown to model internal, enriched and indexed category theory. This means that while the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensures that all proofs and constructions carry over to these generalized settings as well.

## Accelerated Information Dissemination on Networks with Local and Global Edges

Martin Krejca (LIX)
Thursday 13 October 2022 at 11:30, room Nicolaas Govert de Bruijn
Invited by the AlCo team.

“Bootstrap percolation is a classical model for the spread of information in a network. In the round-based version, nodes of an undirected graph become active once at least r neighbors were active in the previous round. We consider a slightly modified variant, acting on graphs that contain two types of edges—modeling local and global interactions, respectively. In this model, information spreads immediately via local edges but still requires a certain number r of active neighbors in order to spread via global edges. We show for certain graph classes that this modified process, when starting with a single active node, results in a phase transition with respect to how quickly further nodes are activated. Initially, the spread is rather slow, but it gains significant speed once global edges are being used to activate nodes.”

## Crossover for Cardinality-Constrained Optimization

Simon Wietheger (Hasso Plattner Institute)
Friday 7 October 2022 at 11:30, room Poincaré
Invited by the AlCo team.

“In order to understand better how and why crossover can benefit optimization, we consider pseudo-Boolean functions with an upper bound 𝐵 on the number of 1s allowed in the bit string (cardinality constraint). We consider the natural translation of the OneMax test function, a linear function where 𝐵 bits have a weight of 1 + 𝜀 and the remaining bits have a weight of 1. The literature gives a bound of Θ(𝑛^2) for the (1+1) EA on this function. Part of the difficulty when optimizing this problem lies in having to improve individuals meeting the cardinality constraint by flipping both a 1 and a 0. The experimental literature proposes balanced operators, preserving the number of 1s, as a remedy. We show that a balanced mutation operator optimizes the problem in 𝑂 (𝑛 log 𝑛) if,𝑛 − 𝐵 = 𝑂 (1). However, if 𝑛 − 𝐵 = Θ(𝑛), we show a bound of Ω(𝑛^2), just as classic bit flip mutation. Crossover and a simple island model gives 𝑂 (𝑛^2/log 𝑛) (uniform crossover) and 𝑂 (𝑛√𝑛) (3-ary majority vote crossover). For balanced uniform crossover with Hamming distance maximization for diversity we show a bound of 𝑂 (𝑛 log 𝑛).”

## Combinatorial Flows as Bicolored Atomic Flows

Giti Omidvar (LIX)
Monday 5 September 2022 at 14:00, online seminar
Invited by the PARTOUT team.

We introduce a new graphical representation of proofs which we call combinatorial flows. They can be seen as a generalization of atomic flows on one side and of combinatorial proofs on the other side. They inherit the close correspondence with open deduction and the possibility of tracing atom occurrences from atomic flows, introduced by Guglielmi and Gundersen. The correctness criterion, on the other hand, is inherited from combinatorial proofs, introduced by Hughes. Hence, combinatorial flows form a proof system in the sense of Cook and Rackhow. In this talk, I will show how to translate an open deduction derivation to a combinatorial flow. Moreover, I will introduce a normalization process for combinatorial flows with units.

## A positive perspective on term representation

Jui-Hsuan Wu (Ray) (LIX)
Monday 27 June 2022 at 14:00, online seminar
Invited by the PARTOUT team.

The structure of terms and expressions are represented variously via, say, labeled trees or directed acyclic graphs (DAGs). When such expressions contain bindings, additional devices are needed. In this talk, I will present the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative bias, LJF proofs encode term structures as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive bias, LJF proofs yield a structure in which explicit sharing of term structures is possible. In this situation, cut elimination yields a different notion of substitution. To illustrate these two approaches to term representation, I will give an example by applying them to the encoding of untyped λ-terms.

## Analog characterization of complexity classee

Riccardo Gozzi (LIX)
Tuesday 21 June 2022 at 11:00, room Grace Hopper
Invited by the AlCo team.

In the first part of the presentation I will introduce the concept of analog computation in relation with integrator devices used in the 1940’s to compute simple operations, called differntial analyzers. A description of the theoretical model behind the behaviors of those machine was first provided by Shannon, with his GPAC model which stands for Generable Purpose Analog Computation model. I will describe some of the main modifications that have been later applied in litterature to the model in order to simplify its formulation and improve its computational power. Following this guideline, I will then explain how these modifications led to an equivalence between this model and the setting of computable analysis, meaning that every function that can be computed within the computable analysis framework can also be computed by the GPAC model, and viceversa. During the course of this first, introductory, part of the talk, the motivations at the core of this research will be discussed as well. In the second part of the presentation I will illustrate how, with the correct improvements to the notion of computation of the GPAC model, this particular equivalence can be extended to the case of polynomial time complexity, leading to an equivalence between the well known complexity calss P and a certain class of systems of ODEs. To obtain this result it is required a way to encode and reproduce the behavior of the transiction function of a Turing machine in a continuous setting, keeping bounded the error introduced during this simulation.This second part of the talk will be more quantitative than the first, including more technical details. Finally, in the last part of the presentation, I will briefly mention how the results previuosly showed can be applied to further characterize higher complexity classes, such as EXPTIME or PSPACE, with similar dynamical system.

## A First Runtime Analysis of the NSGA-II on a Multimodal Problem

Zhongdi QU (LIX)
Tuesday 21 June 2022 at 14:00, room Philippe Flajolet
Invited by the AlCo team.

Very recently, the first mathematical runtime analyses of the multi-objective evolutionary optimizer NSGA-II have been conducted (AAAI 2022, GECCO 2022 (to appear), arxiv 2022). We continue this line of research with a first runtime analysis of this algorithm on a benchmark problem consisting of two multimodal objectives. We prove that if the population size $N$ is at least four times the size of the Pareto front, then the NSGA-II with four different ways to select parents and bit-wise mutation optimizes the OneJumpZeroJump benchmark with jump size $2 \le k \le n/4$ in time $O(N n^k)$. When using fast mutation, a recently proposed heavy-tailed mutation operator, this guarantee improves by a factor of $k^{\Omega(k)}$. Overall, this work shows that the NSGA-II copes with the local optima of the OneJumpZeroJump problem at least as well as the global SEMO algorithm.

## Investigating lenses between preordered sets

Bryce Clarke (LIX)
Monday 20 June 2022 at 14:00, online seminar
Invited by the PARTOUT team.

Bidirectional transformations are a means of maintaining consistency between a pair of systems. In 2005, the mathematical structure of a lens was introduced to model bidirectional transformations, and has since grown into an active topic of research in computer science and applied category theory. Classically, a system may be modelled by its set of possible states, leading to a particular notion of lens, however as more sophisticated models of systems have developed, more interesting and useful notions of lens have arisen.

The aim of this talk is to investigate lenses between preordered sets. The principal idea is that a system is modelled by its set of states equipped with a preorder, which specifies when one state may transition to another, while a lens is an order-preserving function with certain additional structure. Throughout the talk we will explore answers to several natural questions regarding the mathematical structure of lenses. How do lenses compose and decompose, both sequentially and in parallel? What are the ways in which we can build new lenses with nice properties? Given an order-preserving function, how many lens structures does it admit, and is it possible to freely generate a lens structure from it? The talk will focus on demonstrating answers to these questions via small “toy” examples, and aims to be accessible without prior knowledge of category theory. If time allows, I will discuss how the framework of lenses may be extended when systems are instead modelled by generalised metric spaces or weighted categories.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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 (Reykjavik University)
Monday 18 October 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.

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

## 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.

## 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.

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

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.

## 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

## 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.

## 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.

## 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 (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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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 https://github.com/miki-hermann/mcp.

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

## 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.

## 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.

## 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)

## 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.