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.

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

TBA

Alex Kavvos (Bristol)
Wednesday 23 June 2021 at 14:00, online seminar
Invited by the Partout team.
Krzysztof Ziemiański

Tracks in Higher Dimensional Automata

Krzysztof Ziemiański (University of Warsaw)
Wednesday 23 June 2021 at 11:00, online seminar
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
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 https://github.com/miki-hermann/mcp.

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