Seminar
The seminar is joint between AlCo, Cosynus and Partout teams of LIX. To keep informed you can
 subscribe to the mailinglist
 subscribe to the calendar
 read the mail announce for next seminar (or specifically the one of AlCo, Cosynus or Partout)
 read the mail announce for the one following next seminar (or specifically the one of AlCo) read a tweet like announce for next seminar (or specifically the one of AlCo, Cosynus or Partout)
Linear Hybrid Systems are Hard: The Case of Linear Complementarity Systems and The Quest For Characterizing Qmatrices
Khalil Ghorbal (INRIA Rennes)Friday 24 November 2023 at 10:00, room Grace Hopper
Invited by the Cosynus team.
Linear complementarity systems (LCS) form a special class of linear hybrid systems with an exponential number of modes and a linear differential algebraic equation in each mode. While seemingly simple, little is known about the existence (and uniqueness) of continuous solutions for LCS. The only known sufficient condition is rather strong and requires the existence and uniqueness of solutions for the underlying linear complementarity problem (LCP) which, for a fixed matrix M and a given vector q, asks whether there exists a pair of vectors (w,z) satisfying w  M z = q, w,z >= 0, and w.z = 0. M is said to be a Qmatrix when a solution exists for all q. We start by exposing the inherent difficulty of characterizing Qmatrices by reformulating the problem as a covering problem of R^n. We then investigate the regions where no solution exists (so called holes) and show that they only occur in specific locations. This property is exploited to fully characterize planar and spatial Qmatrices via a local reduction around the vectors defining the problem.
This is a joint work with Christelle Kozaily.
Khalil Ghorbal is an INRIA researcher in Rennes, with the Hycomes group.
Guaranteed numerical methods to secure a zone with autonomous robots
Luc Jaulin (LabSTICC)Friday 10 November 2023 at 14:00, room Grace Hopper
Invited by the Cosynus team.
In this talk, we provide an intervalbased method to prove that there are no submarine intruders inside a zone of the ocean (here the Bay of Biscay). For this purpose, a group of underwater robots will be used. We assume that

Our robots are able to localize themselves with a given accuracy.

They are able to communicate at a low rate at low distances.

Each robot is able to detect any intruder inside a disk of a known radius.

The speed of the intruders is assumed to be bounded and is small with respect to that of our robots.
Our goal is twofold:

to characterize a set for which we can guarantee that there is no intruder (this corresponds to the secure zone)

to find a control strategy for the group of robots in order to extend the secure zone as much as possible.
Luc Jaulin is a full professor at Université de Bretagne Occidentale and in charge of the autonomous robotics specialization at ENSTA Bretagne.
Directed homology and persistence modules
Éric Goubault (LIX)Tuesday 17 October 2023 at 11:00, room Grace Hopper
Invited by the Cosynus team.
In this talk, we will try to give a selfcontained account on a construction for a directed homology theory based on modules over algebras, linking it to both persistence homology and natural homology.
Persistence modules have been introduced originally for topological data analysis, where the data set seen at different « resolutions » is organized as a filtration of spaces. This has been further generalized to multidimensional persistence and « generalized » persistence, where a persistence module was defined to be any functor from a partially ordered set, or more generally a preordered set, to an arbitrary category (in general, a category of vector spaces).
Directed topology has its roots in a very different application area, concurrency and distributed systems theory rather than data analysis. Its goal is to study (multidimensional) dynamical systems, discrete (precubical sets, for application to concurrency theory) or continuous time (differential inclusions, for e.g. applications in control), that appear in the study of multiagent systems. In this framework, topological spaces are « directed », meaning they have « preferred directions », for instance a cone in the tangent space, if we are considering a manifold, or the canonical local coordinate system in a precubical set. Natural homology, an invariant for directed topology, defines a natural system of modules, a further categorical generalization of (bi)modules, describing the evolution of the standard (simplicial, or singular) homology of certain path spaces, along their endpoints. Indeed, this is, in spirit, similar to persistence homology.
This talk will be concerned with a more « classical » construction of directed homology, mostly for precubical sets here, based on (bi)modules over (path) algebras, making it closer to classical homology with value in modules over rings, and of the techniques introduced for persistence modules. Still, this construction retains the essential information that natural homology is unveiling. Of particular interest will be the role of restriction and extension of scalars functors, that will be central to the discussion of Kunneth formulas and relative homology sequences. If time permits as well, we will discuss some « tameness » issues, for dealing with practical calculations.
Éric Goubault is a full professor at École Polytechnique.
Constructor unboxing
Gabriel Scherer (LIX)Monday 2 October 2023 at 11:00, room Grace Hopper
Invited by the PARTOUT team.
In this work I will present a new feature proposed for the OCaml programming language, “constructor unboxing”, first suggested by Jeremy Yallop in March 2020. It enables a more efficient representation of certain sum types, but requires a static analysis to forbid certain unboxing requests that would be unsound.
To define this static analysis, one has to solve a problem of normalization of firstorder definitions in presence of recursion. In the talk I hope to explain my current understanding of this halting problem, and present an algorithm to compute normal forms and reject (in finite time) nonnormalizable definitions.
Gabriel Scherer is an Inria researcher at LIX.
Mechanizing SessionTypes Using a Structural View — Enforcing linearity without linearity
Brigitte Pientka (McGill University)Monday 25 September 2023 at 11:00, room Grace Hopper
Invited by the PARTOUT team.
Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higherorder abstract syntax to handle channel mobility and the intricate binding structures that arise in session typed systems.
Following this approach, we mechanize a sessiontyped system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as sessiontyped languages.
Brigitte Pientka is a Full Professor in the School of Computer Science at McGill University, and leading the Computation and Logic group. She received her PhD from Carnegie Mellon University in 2003, and studied previously at the University of Edinburgh and Technical University of Darmstadt.
Applications of Homological Algebra to Algebraic Theories
Mirai Ikebuchi (Kyoto University)Wednesday 20 September 2023 at 15:00, room Grace Hopper
Invited by the Cosynus team.
It is wellknown that some algebraic theories such as groups or Boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given algebraic theory (or term rewriting system), using homological algebra. In this talk, I develop the homology theory for term rewriting systems more and provide a better lower bound under the constraint that the set of function symbols is fixed. Also, the same methodology applies to equational unification, the problem of solving an equation modulo equational axioms. I provide a relationship between equational unification and homological algebra for algebraic theories: Equational unifiability implies the surjectivity of a homomorphism of abelian groups associated with the algebraic theory and the equation to solve.
Mirai Ikebuchi is assistant professor at Kyoto University.
Optimal Runtime Assurance
Sayan Mitra (University of Illinois at UrbanaChampaign)Tuesday 11 July 2023 at 11:00, room Amphi R111, ENSTA Paris
Invited by the COSYNUS team.
A runtime assurance system (RTA) enables the exercise of an untrusted controller while assuring safety with a backup (or safety) controller. The relevant computational design problem is to create a logic that assures safety by switching to the safety controller as needed, while maximizing some performance criteria, such as the utilization of the untrusted controller. Existing RTA design strategies are wellknown to be overly conservative and, in principle, can lead to safety violations. In this talk, I will discuss a formulation of the optimal RTA design problem and present a new approach for solving it. The approach relies on reward shaping and reinforcement learning. It can guarantee safety and leverage reinforcement learning for scalability. We have implemented this algorithm and present experimental results comparing our approach with stateoftheart reachability and simulationbased RTA approaches in a number of scenarios using aircraft models in 3D space with complex safety requirements. Our approach can guarantee safety while increasing utilization of the experimental controller over existing approaches. We also note that changing from safety to reachability is nontrivial from the point to view of achieving optimal memoryless policies with reward shaping.
Sayan is a Professor and John Bardeen Faculty Scholar of Electrical and Computer Engineering, and an Associate Director of the Center for Autonomy, at the University of Illinois, UrbanaChampaign. Sayan received his Ph.D. from MIT, and his research is on formal verification and safe autonomy. His group is known for developing algorithms for datadriven verification and synthesis, some of which are being commercialized. His textbook on the verification of cyberphysical systems was published in 2021. Former Ph.D. students from his group are now professors at Vanderbilt, NC Chapel Hill, MIT, and WashU. His group’s work has been recognized with ACM Doctoral Dissertation Award, NSF CAREER Award, AFOSR Young Investigator Prize, and several best paper awards.
Measuring robustness of dynamical systems. Relating time and space to length and precision
Manon Blanc (LIX)Wednesday 28 June 2023 at 10:00, room Grace Hopper
Invited by the ALCO team.
Verification of discrete time or continuous time dynamical systems is known to be undecidable. However, undecidability is known not to hold for robust systems: if robustness is defined as the fact that the reachability relation is stable under infinitesimal perturbation, then decidability holds. Similarly, while undecidability holds for logical formulas over the reals, it does not when considering deltaundecidability, i.e. when properties are either true or deltafar from being true. We first relate these notions of robustness. Then, we extend these statements at the complexity level: When a system is robust, it makes sense to quantify at which level of perturbation a system is robust. We prove assuming robustness to polynomial perturbation on precision leads to PSPACE and even to a characterization of PSPACE. We prove assuming robustness to polynomial perturbation on time or length leads to similar statements but with PTIME. We also relate this to analogue models of computation.
A system of inference based on proof search:an extended abstract
Dale Miller (LIX)Wednesday 21 June 2023 at 14:00, online seminar
Invited by the PARTOUT team.
Gentzen designed his natural deduction proof system to “come as close as possible to actual reasoning.” Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. PSF (Proof Search Framework) attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated. This is a practice talk for my presentation at LICS 2023, see the accompanying paper.
Autonomous systems in the intersection of formal methods,learning, and controls
Ufuk Topcu (Department of Aerospace Engineering and Engineering Mechanics at The University of Texas at Austin)Tuesday 13 June 2023 at 11:00, room Salle Sophie Germain, LIX, Bâtiment Alan Turing
Invited by the COSYNUS team.
Autonomous systems are emerging as a driving technology for countlessly many applications. Numerous disciplines tackle the challenges toward making these systems trustworthy, adaptable, userfriendly, and economical. On the other hand, the existing disciplinary boundaries delay and possibly even obstruct progress. I argue that the nonconventional problems that arise in designing and verifying autonomous systems require hybrid solutions at the intersection of learning, formal methods, and controls. I will present examples of such hybrid solutions in the context of learning in sequential decisionmaking processes. These results offer novel means for effectively integrating physicsbased, contextual, or structural prior knowledge into datadriven learning algorithms. They improve data efficiency by several orders of magnitude and generalizability to environments and tasks that the system had not experienced previously. I will conclude with remarks on a few promising future research directions
Ufuk Topcu is an Associate Professor in the Department of Aerospace Engineering and Engineering Mechanics at The University of Texas at Austin, where he holds the W. A. “Tex” Moncrief, Jr. Professorship in Computational Engineering and Sciences I. He is a core faculty member at the Oden Institute for Computational Engineering and Sciences and Texas Robotics and the director of the Autonomous Systems Group. Ufuk’s research focuses on the theoretical and algorithmic aspects of the design and verification of autonomous systems, typically in the intersection of formal methods, reinforcement learning, and control theory.
Computation in logic as the splitting of idempotents in algebraic geometry; two models of multiplicative linear logic
Will Troiani (LIPN)Thursday 1 June 2023 at 15:00, room Philippe Flajolet
Invited by the Cosynus team.
A hypersurface f = 0 in complex affine space is singular if and only if there exists a noncontractible matrix factorization of f (to be defined in the talk). Matrix factorisations are organised into a bicategory where composition is defined via a twostep process, first an infinite model of the composite is described, and then a terminating procedure is followed to extract a finite presentation. Is this terminating procedure a semantics of cutelimination? By considering simple cases, Daniel Murfet and myself have uncovered two models of multiplicative linear logic, one in the space of coordinate rings where cutelimination corresponds to the celebrated Buchberger Algorithm, and the other in the space of Quantum Error Correction Codes, where cutelimination corresponds to quantum error correction. The general picture has led Murfet and myself to postulate that the splitting of idempotents has fundamental relevance to the theory of computation. This talk defends this proposition.
From Game Semantics to Species of Structures
Hugo Paquet (LIPN  Université Sorbonne Paris Nord)Wednesday 19 April 2023 at 14:00, room Philippe Flajolet
Invited by the PARTOUT team.
In this talk I will discuss the connections between two different models for programming languages: a semantics based on games and strategies, and a combinatorial semantics based on profunctors and generalized species of structures. A formal comparison is challenging, because these models provide two different representations of effects and resources. For effects, both models use a linear continuation monad, but one is polarized while the other isn’t. For resources, both models use a linear exponential comonad, but one saturates under resource symmetries, while the other picks canonical representatives for symmetry classes. The main technical result is a bicategorical functor from strategies to species of structures. This highlights the key differences, and can be used to transport results from one model to the other. This is based on joint work with P. Clairambault and F. Olimpieri.
Non Determinism in Spatialized Systems, Generically
Luidnel Maignan (Université ParisEst Créteil / Université ParisSaclay)Tuesday 11 April 2023 at 15:00, room Philippe Flajolet
Invited by the Cosynus team.
In my works with Antoine Spicher and Alexandre Fernandez, we consider an abstraction of space where we only think of it through the way it limits the knowledge you can have about the state of a system. This is formalized through a category of object representing something similar to a knowledge state about the system. In a recent MFCS paper, we showed that nondeterminism is, in some categorical sense, a particular case of the general definition. We did it on the concrete example of nondeterministic Lindenmeyer systems, and showed how the 2monad of families is necessary to express this abstraction. For this presentation, I would also like to quickly explain how this is related to different categorical constructions: presheaves, profunctors, and left fibrational spans.
Monadic rewriting systems and the word problem
CarlFredrik Nyberg Brodda (Université Gustave Eiffel)Wednesday 5 April 2023 at 14:00, room Salle Grace Hopper + BBB (recording available)
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. Languagetheoretic methods can be used to study it, which has revealed deeps links in group theory between accessible groups, virtually free groups, the geometry of contextfree graphs, and contextfree 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 nonconstructive – but highly algebraic – definition of the class of all contextfree 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 Flajolet (recording available)
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 lambdacalculus and of system L in the style of Curien, Herbelin and MunchMaccagnoni. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on the notion of nonuniform 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 AverageCase 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 averagecase analysis is that we do not actually know the probability distribution of realworld 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 realworld 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 realworld 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 realworld 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 #Pcomplete. However, in the specific case of planar graphs, the FKTalgorithm 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 ZWcalculus, a graphical language inspired by two kinds of entanglement, the GHZstates and Wstates. 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 ZWcalculus. It appears that reformulating matchgate theory into the categorytheoretic framework of ZWcalculus allows for a much simpler presentation. Conversely, the matchgate approach provides the ZWcalculus with a straightforward combinatorial interpretation. I will introduce a fragment of ZWcalculus, the planar Wcalculus, 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 simplytyped secondorder syntax, linear syntax, or (intrinsic) polymorphic syntax such as system F.
TwoDimensional 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 treelike 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 lambdaterms. We also exploit concurrency theory techniques—traces and simulation—to compare untyped lambdaterms using different structuring disciplines. [This is joint work with JuiHsuan 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 lowlevel 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
Mehrnoosh Sadrzadeh (University College London)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
HsienKuei 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 cutelimination 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: cutelimination 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 cutelimination 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 cutelimination 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 proofchecking 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., selfsufficient provers that trust proofs only when they are checked by their kernel—to an explicitly nonautarkic 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 offtheshelf webbased technologies, such as JSON, IPFS, IPLD, and public key cryptography.
Verification of cyberphysical systems: a counterexampleguided approach
Guillaume Berger (LIX)Thursday 20 October 2022 at 09:00, room Henri Poincaré
Invited by the Cosynus team.
We study counterexampleguided methods to compute stability and safety certificates for hybrid linear systems. Counterexampleguided 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 fixedcomplexity and an adaptivecomplexity template. In the fixedcomplexity template, the number of linear pieces of the certificate is fixed; while in the adaptivecomplexity 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 correctbydesign 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 cyberphysical 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 righthand 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 setbased 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 roundbased 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 CardinalityConstrained 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 pseudoBoolean 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 𝑂 (𝑛√𝑛) (3ary 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
JuiHsuan 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 treelike 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 NSGAII 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 multiobjective evolutionary optimizer NSGAII 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 NSGAII with four different ways to select parents and bitwise 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 heavytailed mutation operator, this guarantee improves by a factor of $k^{\Omega(k)}$. Overall, this work shows that the NSGAII 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 orderpreserving 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 orderpreserving 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 draganddropping 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 socalled “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, dualintuitionistic, biintuitionistic 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 higherorder computation with “reader/writer” effects: state, input/output, probabilities, and nondeterminism. The main result is to extend two fundamental properties of the lambdacalculus to these effects: reduction in the FMC is confluent, and a system of simple types confers strong normalization.
The premise is to view the lambdacalculus 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 kappacalculus and from concatenative programming languages, and enables the encoding of reduction strategies, including callbyvalue lambdacalculus, and for the given effects, Moggi’s metalanguage, Levy’s callbypushvalue, 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.
Higherorder algebraic theories
Dylan McDermott (Reykjavik University)Monday 9 May 2022 at 15:30, online seminar (slides available)
Invited by the Partout team.
Firstorder algebraic theories describe algebraic structures that can be presented by a collection of operators and equations. These were generalized by Fiore et al. to secondorder algebraic theories, in which the operators can bind simple variables. Examples include lambdaabstraction in the untyped lambdacalculus, and quantification in firstorder logic.
We generalize to higherorder theories, in which operators can bind variables of higher orders. I will discuss the resulting notion of nthorder algebraic theory, and some examples. Nthorder 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)thorder algebraic theories and certain monads on nthorder algebraic theories, analogous to the correspondence between (monosorted) firstorder theories and finitary monads on Set.
This is joint work with Nathanael Arkor.
Neural Networks with PhysicsInformed 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 physicsbased 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 AbstractionBased 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 cyberphysical systems using abstractionbased control synthesis approaches. These approaches first create a finitestate 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. Abstractionbased control synthesis techniques allow us to handle complex dynamics of CPS models and nontrivial 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 sousshift (ou sousdé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 fanin. In some sense, the search for such a classification concentrates most of the open questions we have about the relationship between NC1 and its wellstudied 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 fanin. This characterisation takes the form of a triple languagesalgebralogic correspondence: a regular language is in AC0 if and only if its syntactic morphism is quasiaperiodic if and only if it is definable in firstorder 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 stackheightbehaviour 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 Extalgebras, an extension of recognisability by monoidmorphisms 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 Extalgebramorphisms that recognise them:
 those that are TC⁰hard;
 those that are in AC⁰;
 those that correspond to a wellidentified 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 proofsasprograms 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 nonequivalent, 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 realworld 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 estimationofdistribution 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 continuousvariable 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 nonGaussianity 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 MarcelPaul Schützenberger (recording available)
Invited by the Partout team.
[Organizer’s note: this will be a hybrid seminar, simultaneously taking place at Salle MarcelPaul Schützenberger and on BBB.]
By abstracting over wellknown properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and captureavoiding 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
List monads
Tarmo Uustalu (Reykjavik University)Monday 18 October 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.
We tend to speak of the (possibly empty) list monad and the nonempty list monad, meaning the free monoid monad and the free semigroup monad, as if those were the only monad structures on the list and nonempty list endofunctors (on Set). But they are not! It may at first seem hard to construct other list and nonempty list monads, but at a closer look it turns out that examples abound. There are infinitely many list monads with the singleton function as the unit that admit a presentation with one nullary and one binary operation, and infinitely many nonempty list monads with singleton as the unit and a presentation with one binary operation; some multiplications not only delete, but even duplicate and permute elements. There are list and nonempty list monads with singleton as the unit that have no finite presentation. There are nonempty list monads whose unit is the doubleton function. You cannot tell if a nonempty list monad presented to you as a blackbox is the free semigroup monad by testing the unit and multiplication on finitely many inputs. Etc. We are far from having classified all list monads or all nonempty list monads, but these are cool combinatorial problems.
This is joint work with Dylan McDermott and Maciej Piróg.
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 modelchecking, to SMTbased proofs. Also, they apply to various classes of programs from concurrent data types, to distributed databases, or applications thereof.
Historyaware 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 splitbisimulation. One can also add backwardlooking modalities (i.e., past modalities) so to increase the expressiveness so to be able to capture the hereditary historypreserving bisimulation. Classical examples from the literature that are used to distinguish oneoranother 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 ωContextFree 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 contextfree languages of infinite words, a generalization of ωcontextfree languages (Cohen, Gold 1977) and an extension of weighted contextfree languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted contextfree 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 contextfree languages to weighted contextfree languages.
This talk is based on this article and its corresponding short version.
Distributed Denial of Service cyberattacks in 5G networks: a robust approximation approach
Sonia Vanier (Délégation au LIX, et Université Paris, PanthéonSorbonne)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 ongoing 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 subproblem is solved by a Branch & Price algorithm. The results of our computational experiments, carried out on mediumsize randomly generated instances, show that the proposed solution approach is able to provide optimal solutions within short computation times
ClientServer 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 clientserver interactions. We also present a sessiontyped functional programming language for clientserver 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 stepsequence 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 distributorsinduced bicategorical models of lambdacalculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2monads 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 proofrelevant 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.
On Monadic Rewriting Systems
Francesco Gavazzo (University of Bologna)Wednesday 19 May 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
Motivated by the study of effectful programming languages and computations, I will introduce the theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, effects being modelled as monads. Such systems are to effectful computations and programming languages what traditional rewriting systems are to pure computations and programming languages. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining mathematically and operationally meaningful notions of monadic rewriting turns out to be simply not possible for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible.
I will answer that question by showing that the socalled weakly cartesian monads precisely describe computational effects for which monadic rewriting is wellbehaved. If monads are given as equational theories, as it is in the case of algebraic effects, a sufficient condition ensuring monadic rewriting to be wellbehaved 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 callbyvalue λcalculus with algebraic effects, this way obtaining the extension of the wellknown 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 domainspecific 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 Lipschitzcontinuous vector fields using the PicardLindelö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 ZXcalculus
Renaud Vilmart (LMF, ENS ParisSaclay)Wednesday 14 April 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
The ZXCalculus 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.
TimeOptimal SelfStabilizing Leader Election in Population Protocols
Janna Burman (LISN, Université ParisSaclay)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 selfstabilizing 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 selfstabilizing 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 selfstabilizing leader election in asymptotically optimal expected parallel time of O(log n), but using at least exponential states (a quasipolynomial 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 Ktrivialité
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 “Ktriviales” sont celles dont la complexité de Kolmogorov de leurs préfixes est minimale. La classe des Ktriviaux est dénombrable, et contient “juste un peu plus” que les chaînes binaires infinies calculables. Les nombreuses études sur les Ktriviaux 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 CurryHoward 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 frontend 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.
Gaugeinvariance in celullar automata and multiscales analysis
Giuseppe Di Molfetta (AixMarseille 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 spacetime grid. It is clearly physicslike, 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 stepbystep procedure, to make cellular automata invariant under the local action of a gauge group and the notion of gaugeequivalence 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 noncommutative 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 databasebacked 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 polynomialtime checkable while prefix consistency and snapshot isolation are NPcomplete in general. These results complement a previous NPcompleteness result concerning serializability. Moreover, in the context of NPcomplete 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 databasebacked applications. MonkeyDB supports a KeyValue 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 lambdacalculus 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 lambdacalculus is the model of computation underlying functional programming languages and proof assistants. Actually, there are many lambdacalculi, depending on the evaluation mechanism (e.g., callbyname, callbyvalue, callbyneed) and computational feature that the calculus aims to model (e.g., plain functional, nondeterministic, 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 metatheory of lambdacalculi, where the study is rooted on a unique core language, the bang calculus, a variant of the lambdacalculus inspired by linear logic: a bang operator marks which resources can be duplicated or discarded.
The bang calculus subsumes both callbyname and callbyvalue. A property studied in the bang calculus is automatically translated in the corresponding property for the callbyname lambdacalculus and the callbyvalue lambdacalculus, thanks to two different embeddings of the lambdacalculus 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 NPoptimization 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/mikihermann/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 gluingparallel posets generated from singletons by finitary applications of the two compositions. We show that not only seriesparallel 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.
GentzenMintsZucker 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 CurryHoward correspondence and interpret it as an isomorphism between a category of proofs in intuitionistic sequent calculus and a category of terms in simplytyped λ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 logicocomputational 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 finitestate 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 finitestate automata, based on reinterpreting their usual statetransition 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 onedimensional 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.