Seminar
The seminar is joint between AlCo, Cosynus and Partout teams of LIX. To keep informed you can
- subscribe to the mailing-list
- 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)
HCERES Rehearsal
Alco team (LIX, École Polytechnique)Thursday 12 December 2024 at 14:00, room Philippe Flajolet
Invited by the Alco team.
Everything is in the title, and everybody is welcome.
Generic bidirectional typing for dependent type theories
Thiago Felicissimo (Inria Rennes (Gallinette team))Monday 16 December 2024 at 15:00, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
Bidirectional typing is a discipline in which the typing judgment is decomposed into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining mostly informal and not fully developed. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. We also establish the decidability of bidirectional typing for normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype, available at https://github.com/thiagofelicissimo/BiTTs, and used in practice with many theories.
Trigonometry Without π
Daniel de Rauglaudre (INRIA Paris (retired))Wednesday 11 December 2024 at 13:30, room Grace Hopper
Invited by the COSYNUS team.
This talk presents a constructive approach to trigonometry, fully formalized and proven in the Coq proof assistant. Angles are defined as pairs consisting of their cosine and sine. Along the way, some classical trigonometric formulas naturally emerge. The process culminates in the definition of dividing an angle by an integer, achieved through a convergent sequence. No prior knowledge of Coq is required to understand the talk, as no Coq code appears in the slides. While the talk is given in French, the slides are in English, allowing non-French speakers with a basic understanding of French to follow along.
Higher-Order Bayesian Networks
Gabriele Vanoni (IRIF)Monday 9 December 2024 at 13:30, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
Bayesian networks (BNs) are graphical first-order probabilistic models that allow for a compact representation of large probability distributions, and efficient inference, both exact and approximate. We introduce a higher-order programming language, in the idealized form of a lambda-calculus, which we prove sound and complete w.r.t. BNs: each BN can be encoded as a term, and conversely each (possibly higher-order and recursive) program of ground type compiles into a BN. Moreover, we provide a compositional and cost-aware semantics which is based on factors, the standard mathematical tool used in Bayesian inference. Our results rely on advanced techniques rooted into linear logic, intersection types, rewriting theory, and Girard’s geometry of interaction, which are here combined in a novel way.
This is joint work with Claudia Faggian and Daniele Pautasso.
Sup, Sum, and Scalars: In Linear Logic and in Non-Linear Logic
Alejandro Diaz-Caro (Inria Loria (Mocqua team) and Universidad Nacional de Quilmes)Monday 2 December 2024 at 13:30, room Grace Hopper
Invited by the PARTOUT team.
In [1], we introduced a new connective, called “sup”, to intuitionistic propositional logic to model information erasure, non-reversibility, and non-determinism, as observed in quantum measurement, among other contexts. This connective features the introduction rule of conjunction and the elimination rule of disjunction, resulting in a non-deterministic cut-elimination process. To enrich its proof terms, we added a sum operator, which allows for recovering the determinism of the connective. Additionally, since one of our goals was to express quantum programs, we introduced a scalar product. These rules may occupy the space between the introduction and elimination of a given connective, forcing us to include commuting cuts to establish a proper introduction theorem.
The next step toward transforming this calculus into a quantum calculus was to adopt a linear logic framework. Thus, in [2], we considered the full intuitionistic multiplicative-additive linear logic (IMALL). We demonstrated that, when removing the sup connective, the system–augmented with sums and scalar multiplication–is linear in the algebraic sense. Specifically, any term t applied to a linear combination a⋅r+b⋅s is observationally equivalent to a⋅(tr)+b⋅(ts).
In [3], we provided an abstract characterization of the sup connective in IMALL, showing that any symmetric monoidal closed category with biproducts and a monomorphism from the semiring of scalars to the semiring Hom(I,I) is a suitable model. By leveraging the binary biproducts, we defined a weighted codiagonal map, which serves as the core of the sup connective.
Finally, in [4], we considered two non-linear systems: first, with the sum operator alone as a parallel operator, and second, with the combination of the sum and scalar operators as an algebraic lambda calculus. We proposed two categorical models for these calculi. In particular, we explored the role of disjunction within the calculus, which has rarely been studied in conjunction with the parallel (or sum) construct. For the parallel lambda calculus, we employed the category MagSet, whose objects are magmas and whose morphisms are functions from the category Set. For the algebraic lambda calculus, we used the category AMagSSet, whose objects are action magmas, with morphisms similarly drawn from Set. Our approach diverges from conventional interpretations, which typically handle disjunctions via coproducts. Instead, we proposed handling them through a combination of disjoint unions and Cartesian products.
References:
- A. Díaz-Caro and G. Dowek. A new connective in natural deduction, and its application to quantum computing. TCS 957:113840, 2023.
- A. Díaz-Caro and G. Dowek. A linear linear lambda-calculus. MSCS FirstView:1-15, 2024.
- A. Díaz-Caro and O. Malherbe. The Sup Connective in IMALL: A Categorical Semantics. arXiv:2205.02142, 2024.
- A. Díaz-Caro and O. Malherbe. Parallel and algebraic lambda-calculi in intuitionistic propositional logic. arXiv:2408.16102, 2024.
Evolutionary Algorithms Are Robust to Noise out of the Box
Denis Antipov (LIP6, Sorbonne Université)Wednesday 27 November 2024 at 10:30, room Philippe Flajolet
Invited by the ALCO team.
Randomized search heuristics (RHSs) are generally believed to be robust to noise. However, almost all mathematical analyses on how RSHs cope with a noisy access to the objective function assume that each solution is re-evaluated whenever it is compared to others. This is unfortunate, both because it wastes computational resources and because it requires the user to foresee that noise is present (as in a noise-free setting, one would never re-evaluate solutions). In this work, we show the need for re-evaluations could be overestimated, and in fact, detrimental. For the classic benchmark problem of how the (1+1) evolutionary algorithm optimizes the LeadingOnes benchmark, we show that without re-evaluations up to constant noise rates can be tolerated, much more than the O(n^{-2} log n) noise rates that can be tolerated when re-evaluating solutions. This first runtime analysis of an evolutionary algorithm solving a single-objective noisy problem without re-evaluations could indicate that such algorithms cope with noise much better than previously thought, and without the need to foresee the presence of noise.
Strict CwFs for Proving Normalisation
Loïc Pujet (University of Stockholm)Monday 25 November 2024 at 13:30, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
Categories with families (CwF) are perhaps the most widely used notion of models for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant. In this talk, I will present a method based on Pédrot’s “prefascist sets” to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to proofs of canonicity and normalisation by Gluing. This is joint work with Ambrus Kaposi.
A recipe for the semantics of reversible programming
Louis Lemonnier (University of Edinburgh)Tuesday 12 November 2024 at 14:00, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
In this presentation, we explore the foundational elements required to interpret reversible programming within a categorical framework. We use the symmetric pattern-matching language introduced by Sabry, Valiron, and Vizzotto as a reference point, and we incorporate several improvements. We show that inductive data types and recursion can also be effectively modelled in this setting. However, these results do not straightforwardly extend to the pure quantum case. We provide insights into the challenges encountered and propose potential directions for addressing these limitations, for example with guarded recursion.
(Self) references:
De Morgan toposes and model theory
Yorgo Chamoun (Cosynus)Wednesday 6 November 2024 at 14:30, room Philippe Flajolet
Invited by the Cosynus team.
De Morgan’s law, also known as “weak excluded middle”, is expressed in a Heyting algebra (hence in intuitionistic logic) by the equality ¬x ∨ ¬¬x = 1 for any element x of the algebra. On the other hand, a topos is a “pastiche” category of the category of sets, and therefore admits an internal language that is at least intuitionistic. We can therefore naturally define a De Morgan topos as a topos whose internal logic admits De Morgan’s law, but an “external” approach, without any mention of the internal logic, is possible and is very practical to handle. The aim of this presentation will be to illustrate different facets of these toposes, adopting this external approach. Firstly, we will attempt to establish links with model theory and, more specifically, the amalgamation property, via the notion of classifying topos of a geometric theory. Secondly, we will show how a De Morgan topos can be associated in a more or less canonical way with any topos, and the contributions in this field of the tools recently introduced by Caramello for studying (among other things) the internal locales of a topos.
Mechanised Constructive Reverse Mathematics: The Examples of Completeness, Löwenheim-Skolem Theorems, and Post's Problem
Dominik Kirst (IRIF)Monday 4 November 2024 at 13:30, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
The idea of (constructive) reverse mathematics is to identify natural (sub-classical) axioms that are equivalent to certain mathematical theorems and therefore characterise their logical strength. Especially in the constructive case, this research programme highly depends on the choice of base theory, for which we employ the calculus of inductive constructions, and benefits from mechanisation, for which we use the Coq proof assistant.
In this talk, I will give an overview of some ongoing projects concerning Gödel’s completeness theorem for first-order logic, the related Löwenheim-Skolem theorems, as well as Post’s problem concerning the existence of a semi-decidable yet undecidable Turing degree strictly below the halting problem. Especially the latter exploits a synthetic approach to computability theory available in any constructive foundation, where the reference to an explicit model of computation can be disposed of by simply considering every function to be computable.
Craig-Lyndon interpolation as cut-introduction and its computational content
Alexis Saurin (IRIF)Monday 14 October 2024 at 13:30, room Henri Poincaré
Invited by the PARTOUT team.
After Craig’s seminal results on interpolation theorem, a number and variety of proof-techniques, be they semantical or proof-theoretical, have been designed to establish interpolation theorems. Among them, Maehara’s method is specific due to its applicability to a wide range of logics admitting cut-free complete proof systems.
By reconsidering Maehara’s method, I will show how one can extract a “proof-relevant” interpolation theorem for first-order linear-logic stated as follows: if π is a cut-free proof of A⊢B, we can find (i) a formula C in the common vocabulary of A and B and (ii) proofs π1 of A⊢C and π2 of C⊢B the proof π′ of A⊢B, obtained by cutting π1 with π2 on C, normalizes to π by cut-reduction.
I will carry out this investigation of proof-relevant interpolation in two frameworks:
First, in the traditional sequent calculus, I will show that interpolation can be organized in two phases: (i) a bottom-up phase which decorates the sequents with a so-called splitting followed by (ii) a top-down phase which solves the interpolation problem, synthesizing the interpolant by cut-introduction. The flexibility of the approach is exploited to carry the interpolation-as-cut-introduction to classical and intuitionistic logics, satisfying Craig as well as Lyndon’s constraints on the vocabulary of the interpolant.
Then, I will move to Curien & Herbelin’s duality of computation framework and prove a computational version of the above result in System L. The computational content of Maehara’s interpolation can therefore be understood as the factorization of a computation into a term and an evaluation context which interact through an interface-type, the interpolant.
After discussing how the result relates to a proof-relevant refinement of Prawitz’ proof of the interpolation theorem in natural deduction discovered by Čubrić in the 90’s for the simply typed λ-calculus, I will explain – depending on time and interest of the audience – how this approach extends to proof-nets, expoiting the correctness criteria, and to circular proofs in logics with fixed-points.
Catégories syntactiques pour le produit tensoriel des motifs de Nori
Bruno Drieux (LIX)Monday 7 October 2024 at 14:00, room Marcel-Paul Schützenberger
Invited by the Cosynus team.
Suivant l’idée originale de Nori, nous proposons une construction, basée sur la logique catégorielle, d’une catégorie abélienne monoïdale symétrique universelle associée à une représentation d’un carquois dans une catégorie d’espaces vectoriels. Nous étudions ensuite la relation entre cette construction et la généralisation de la construction de Nori afin d’établir des critères explicites d’existence de structures sur cette dernière. Nous obtenons en particulier une construction alternative du produit tensoriel des motifs mixtes de Nori.
A strictly linear system for propositional classical logic
Victoria Barrett (LIX)Monday 30 September 2024 at 13:30, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
We present a proof system for a conservative extension of propositional classical logic with decision trees that is strictly linear, based on recent work in subatomic logic. This means that not only there are no structural rules such as contraction and weakening but there are no rules for unit equalities either, and there is no negation. Yet, its classical semantics and proof-theoretic properties can be recovered via an interpretation map at a polynomial cost. Moreover, this system can p-simulate substitution Frege. Those results are made possible primarily by two technical advances: 1) an ‘Eversion Lemma’, that guarantees extreme flexibility in manipulating formulae to match a given logical context, and 2) a form of explicit substitution for derivations into derivations. We argue that this proof system represents a significant step towards a notion of factorisation for proofs. That will hopefully lead us to a semantics of proofs adequate to solve the proof identity problem.
Coma: an intermediate verification language with explicit abstraction barriers
Andrei Paskevich (Inria Saclay (Toccata team) and LRI)Tuesday 24 September 2024 at 14:00, room Philippe Flajolet
Invited by the PARTOUT team.
Coma is a minimalistic algorithmic language designed for deductive verification. It adopts the continuation-passing style which allows us to express in a natural manner the standard control structures — conditionals, loops, subroutine calls, and exception handling — using only three elementary constructions.
The specification annotations in Coma take the form of assertions mixed with the rest of the program code. A special barrier tag is used to separate, inside a subroutine definition, the “interface” part of the code, which should be verified at each call, from the “implementation” part, which is verified only once, for all possible inputs. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification for different execution paths in the code. We can also forgo the barriers entirely for some (or all) of the paths, which effectively inlines the corresponding code during the computation of verification conditions.
Verification conditions for Coma programs are structurally similar to what is generated by the classical weakest-precondition calculus. However, our procedure can also factorize the instances of selected subformulas in the resulting proof obligation, which leads to more compact verification conditions in the style of Flanagan and Saxe.
Measure Theoretic Approach to Formal Languages
Ryoma Sin'ya (Akita University)Friday 13 September 2024 at 14:00, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
A language L is said to be regular measurable if there exists an infinite sequence of regular languages that “converges” to L. This notion was introduced by the speaker in 2021 and used for classifying non-regular languages by using regular languages. In this talk, we describe why this notion was introduced, and give a brief overview of decidability results relating to the measurability on subclasses (local subvarieties) of regular languages, eg., star-free, generalised definite, piecewise-testable, and group languages.
Theoretical Foundations of Evolutionary Diversity Optimisation for Multi-objective Problems.
Denis Antipov (University of Adelaide)Thursday 27 June 2024 at 16:00, room Marcel-Paul Schützenberger
Invited by the ALCO team.
In practical optimisation problems there is often a risk that the best found solutions turn out infeasible for a range of reasons. To avoid the need to re-run optimisation algorithms once such situations occur, it is common to look for a diverse set of good solutions, since the diversity minimises the chances that all of them turn out to be infeasible. This is a much more challenging task, since we perform the search in the space of (multi-)sets of solutions, which significantly increases the dimensionality of the problem compared to the regular optimisation. The evolutionary algorithms (EAs) are well-suited for this task, since they are naturally designed to optimise populations. This approach of using EAs to evolve diverse populations is called evolutionary diversity optimisation (EDO). It was shown to be effective in practice, but the process of EDO (and therefore, the most effective approaches to it) is not well-understood. In this talk we will discuss the (few) theoretical results which exist in this field, focusing mainly on EDO in Multi-objective domain.
Positive Focusing is Directly Useful
Jui-Hsuan Wu (LIX)Thursday 13 June 2024 at 14:00, room Marcel-Paul Schützenberger
Invited by the PARTOUT team.
Recently, Miller and I introduced the positive λ-calculus, a call-by-value λ-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for the implicational fragment of Gentzen’s LJ. The positive λ-calculus stands out among λ-calculi with sharing for a compactness property related to the sharing of variables. In this talk, I will show that—thanks to compactness—the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models.
This is joint work with Beniamino Accattoli.
Faster Approximation Scheme for Euclidean k-TSP
Ernest van Wijland (ENS Paris)Monday 27 May 2024 at 16:00, room Emmy Noether
Invited by the AlCo team.
In the Euclidean $k$-traveling salesman problem ($k$-TSP), we are given $n$ points in the $d$-dimensional Euclidean space, for some fixed constant $d>2$, and a positive integer $k$. The goal is to find a shortest tour visiting at least $k$ points. We give an approximation scheme for the Euclidean $k$-TSP in time $n.2^{O(1/\varepsilon^{d-1})}.(\log n)^{2d^2\cdot 2^d}$. This improves Arora’s approximation scheme of running time $n.k(\log n)^{\left(O\left(\sqrt{d}/\varepsilon\right)\right)^{d-1}}$ [J. ACM 1998]. Our algorithm is Gap-ETH tight and can be derandomized by increasing the running time by a factor $O(n^d)$. This is joint work with Hang Zhou. This work was accepted for publication at the International Symposium on Computational Geometry (SoCG), 2024.
An Example of Quantum Oblivious Computation
Thomas Debris-Alazard (Inria Saclay)Wednesday 22 May 2024 at 10:30, room Philippe Flajolet
Invited by the AlCo team.
Spaces of Obstacle Avoiding Paths
Yuliy Baryshnikov (University of Illinois at Urbana-Champaign)Wednesday 29 May 2024 at 11:00, room Grace Hopper
Invited by the Cosynus team.
A broad class of models deal with spaces of directed paths avoiding some dynamic obstacles. (Examples include concurrency, in computer science, and collision avoidance in control theory.) The topology (say, the homotopy type) of these spaces is not yet well understood.
It turns out, the study of these spaces is in many respects parallel to the theory of linear subspace arrangements. I will outline some recent results, and the key tools used to obtain them, - in particular, the apparatus of diagrams of spaces.
Mathematical informatics
Thomas Seiller (LIPN)Wednesday 15 May 2024 at 14:00, room Grace Hopper
Invited by the PARTOUT team.
What is a model of computation? What is a program, an algorithm? While theoretical computer science has been founded on computability theory, the latter does not answer these questions. Indeed, it is a mathematical theory of computable functions, and does not account for computation itself. A symptomatic consequence is the notion of Turing-completeness. This standard (sole?) equivalence between models of computation is purely extensional: it does only care about what is computed and not how, blind to complexity aspects and the question of algorithmic completeness. More importantly, the theory of computation is continuously growing further from how actual machines compute. I will present a proposal for alternative foundations more faithful to computer science practice and interests. This mathematisation of computer science is grounded within the theory of dynamical systems, focussing on how computation is performed rather than only on what is computed. I will argue that it generalises computability theory while still allowing to recover standard results.
If time permits, I can then explain how this theory can be used to (I will let he audience decide which items will be discussed):
- provide a uniform account of several lower bounds from algebraic complexity and strengthen them
- define static analysis methods which can be implemented in usable tools
- define families of linear realisability models (realisability models for linear logic)
- lead to a semantic approach of implicit computational complexity
- propose a formal definition of the notion of algorithm
Symmetries in constructive mathematics
Vikraman Choudhury (Università di Bologna)Friday 26 April 2024 at 10:30, room Philippe Flajolet
Invited by the Cosynus team.
I this talk, I will discuss the constructive theory of free commutative monoids (or finite multisets), and free symmetric monoidal groupoids, in Univalent Foundations. I will show several applications to computer science: axiomatics of sorting algorithms, differential structure in models of linear logic, and axiomatisation of type isomorphisms in a language for reversible computing.
Categorical structure in combinatorial algebras
Serge Lechenne (ENS Paris-Saclay)Wednesday 24 April 2024 at 14:00, room Philippe Flajolet
Invited by the PARTOUT team.
We investigate a class of combinatory algebras, called ribbon combinatory algebras, in which we can interpret both the braided untyped linear lambda calculus and framed oriented tangles. Any reflexive object in a ribbon category gives rise to a ribbon combinatory algebra. Conversely, From a ribbon combinatory algebra we can construct a ribbon category with a reflexive object, from which the combinatory algebra can be recovered. To show this, and also to give the equational characterization of ribbon combinatory algebras, we make use of the internal PRO construction developed in Hasegawa’s recent work. Interestingly, we can characterize ribbon combinatory algebras in two different ways: as balanced combinatory algebras with a trace combinator, and as balanced combinatory algebras with duality.
Primal Grammars Driven Automated Induction
Miki Hermann (LIX)Wednesday 27 March 2024 at 14:00, room Grace Hopper
Invited by the PARTOUT team.
Automated induction is important for many computer sciences and artificial intelligence applications. However, proof by induction is undecidable and diverges even for small examples, leading to failures in the proving experience.
Many techniques have proposed ad-hoc heuristics to speculate on additional lemmas that hopefully stop the divergence. Although these methods have succeeded in proving interesting theorems, they have significant limitations: in particular, they often fail to find appropriate lemmas, and the provided lemmas may not be valid.
We present a new technique that allows us to perform inductive proofs in conditional theories by automatically detecting the divergence of proof traces and deriving a primal grammar as well as new lemmas that schematize the divergent sequences and, thus, allow breaking the divergence and ending the proof. Our new technique is presented as a set of inference rules whose soundness and refutational completeness have been formally proved. Refutational completeness is particularly useful for detecting flaws in critical systems. Moreover, unlike related work, our new technique has no risk of over-generalization. If the initial conjectures are valid, then the lemmas generated by our technique subsume the divergent sequence and are also valid.
The cornerstone of our method is the use of primal grammars, which are based on primitive recursive functions and represent the most general decidable schematization, with respect to description power, among all known schematizations. Our technique always succeeds in building a primal grammar when the divergence follows a primitive recursive pattern; this allows us to cover a large class of problems.
Our new technique has been implemented in C++ and successfully proved several dozens of complex examples that fail with well-known theorem provers such as ACL2, Isabelle, LEAN, PVS, RRL, SPIKE, and related techniques for capturing and schematizing divergence for proof by induction.
Towards Provably Safe and Secure Systems with Contract-Based Design
Inigo Incer (CMS, Caltech)Thursday 14 March 2024 at 15:00, room Marcel-Paul Schützenberger
Invited by the Cosynus team.
The task of system design is shared by all engineering disciplines, each coming with its own techniques. In spite of their differences in tools, there is large intersection in their conceptual approach to design. In this talk, we exploit this commonality to take an abstract view of systems and their composition. We understand systems and subsystems in terms of their assume-guarantee specifications, or contracts.
Assume-guarantee contracts are formal specifications that state (i) the assumptions that a design element makes on its environment and (ii) the guarantees it delivers when the environment behaves according to the contract’s assumptions. Contracts come with a rich algebra that allows us to carry out several design-relevant tasks: obtaining system-level specifications from component specifications, finding specifications of components that need to be added to a design in order to meet an objective, etc. We will introduce the algebra of contracts and discuss how the various algebraic operations relate to system-design tasks. We will discuss hypercontracts, an extension of assume-guarantee reasoning to support the formal analysis of key security and robustness properties. We will also discuss the application of this methodology and Pacti, a software package that supports system design using contracts, in applications ranging from space-mission design to synthetic biology.
Bio: Inigo Incer is a postdoctoral researcher at Caltech and UC Berkeley. He obtained his PhD from UC Berkeley in 2022 under the guidance of Alberto Sangiovanni-Vincentelli. He is interested in all aspects of cyber-physical systems, emphasizing formal methods and AI that support their compositional design and analysis. Before pursuing a PhD, Inigo was an IC designer in Austin. His work has been supported by the NSF/ASEE eFellows program and the UC Berkeley Chancellor’s Fellowship.
Petri nets, monoidal categories, and linear logic (A survey and some recent results)
Fabio Gadducci (Università di Pisa)Wednesday 13 March 2024 at 14:00, room Grace Hopper
Invited by the PARTOUT team.
In a seminal paper Montanari and Meseguer have shown that an algebraic interpretation of Petri nets in terms of monoids can be used to provide an elegant characterisation of the deterministic computations of a net, accounting for their sequential and parallel composition, in terms of monoidal categories. The same framework was recognised by Asperti as the right one for interpreting the multiplicative fragment of linear logic. In this talk we will give a survey of these classical results, plus adding a novel characterisation for non-deterministic computations of a net in terms of dioidal categories, which are the categorical equivalent of tropical semirings, and suggesting a possible connection with the multiplicative additive fragment of linear logic.
A Categorical Approach to Describing Complexity Classes
Damiano Mazza (LIPN)Wednesday 28 February 2024 at 14:00, room Philippe Flajolet
Invited by the PARTOUT team.
We introduce a categorical framework for describing decision problems and providing machine-independent characterizations of complexity classes, mixing ideas coming from descriptive complexity and categorical logic. The framework is based on the opposite of the category of small Boolean lextensive categories and logical functors. This has nice categorical properties and, crucially, its morphisms may be seen as descriptions of decision problems. The complexity of problems may be controlled by restricting morphisms via suitable algebraic and logical properties, obtaining several well-known classes (recursively enumerable problems, NP, P, NL, P/poly…). If time permits, we will see how this approach leads to considering algebraic objects which generalize commutative rings and affine schemes (in the sense of algebraic geometry).
Context-free grammars and finite-state automata over categories
Noam Zeilberger (LIX)Thursday 15 February 2024 at 10:45, room Marcel-Paul Schützenberger
Invited by the Cosynus team.
A little over a year and a half ago, Paul-André Melliès and I wrote a paper giving a categorical analysis of the so-called Chomsky–Schützenberger representation theorem, whose usual formulation states that “a language is context-free iff it is a homomorphic image of the intersection of a Dyck language with a regular language”. Since then, our understanding of the material has evolved significantly, and we wrote a thoroughly revised and expanded version of the paper: The categorical contours of the Chomsky-Schützenberger representation theorem.
The main message of the paper is that there are natural notions of “context-free grammar” and of “non-deterministic finite state automaton” over arbitrary categories and operads, and that looking at CFGs and NDFAs in this way seems to have some real explanatory power. In the talk I will give some examples, and sketch some of the other ideas and results from the paper.
Univalent foundations for the formalization of (higher) category theory
Benedikt Ahrens (Delft University of Technology)Wednesday 7 February 2024 at 14:00, room Grace Hopper
Invited by the PARTOUT team.
Category theory is a mathematical theory of structures and their interactions. It was originally developed to axiomatize algebraic topology; in the meantime, it has proved useful as a language and infrastructure for organizing knowledge in many areas of mathematics, computer science, data science, biology, and more.
The formulation of category theory in set-theoretic foundations has been seen as problematic: the notion of “sameness” between mathematical objects provided by set theory does not coincide with the fundamental notion of isomorphism in category theory. This divergence is exacerbated when considering higher-categorical structures, such as categories themselves.
In this talk, we explain how univalent foundations provides exactly the right setting in which to formalize category theory. In particular, equivalence of categories coincides with “sameness” of categories in the sense of univalent foundations.
Capacitated Vehicle Routing
Hang Zhou (LIX)Wednesday 31 January 2024 at 10:30, room Philippe Flajolet
Invited by the ALCO team.
In the capacitated vehicle routing problem, we are given a metric space with a vertex called depot and a set of vertices called terminals. The goal is to find a minimum length collection of tours starting and ending at the depot such that each tour visits at most k terminals, and each terminal is visited by some tour. In this talk, I am going to talk about recent progress on the capacitated vehicle routing problem on trees and in the two-dimensional Euclidean plane.
Smooth models of concurrent programs
Emmanuel Haucourt (LIX)Thursday 25 January 2024 at 15:00, room Marcel-Paul Schützenberger
Invited by the Cosynus team.
A sequential program is usually represented by an automaton, i.e. a graph labelled with instructions on which the instruction pointer moves. There is no such consensus about the way of representing concurrent programs. Higher dimensional automata were introduced to this end by Pratt and van Glabbeek in the early 90’s, the first continuous models were proposed by Fajstrup, Goubault and Raussen about a decade later, mixing topology and (local) order. As we will explain during the talk, the two later derive from a non-Hausdorff manifold M equipped with a parallelization (i.e. a tuple of vector fields (f₁,…,fₙ) giving a basis of the tangent space at each point of the manifold). The manifold M even comes with an atlas whose transition functions are mere vector translations; concretely, it means that one can do differential calculus on M (almost) as in the euclidean space ℝⁿ, i.e. without paying attention to charts.
Enriched bisimulations
Matthew di Meglio (University of Edinburgh (LFCS))Wednesday 17 January 2024 at 15:00, room (online)
Invited by the PARTOUT team.
(Joint work with Bryce Clarke)
Bisimulations of Kripke frames, and strong and weak bisimulations of labelled transition systems, are all examples of a more general notion of bisimulation for enriched graphs and enriched categories. I will give a gentle and example-oriented introduction to enriched categories, their bisimulations, and the connection to enriched lenses. We hope that this talk will lead to discussion on further aspects of the theory of Kripke frames and modal logic that could be generalised to the setting of enriched categories.
Matthew di Meglio is a PhD student in the Laboratory for Foundations of Computer Science at the University of Edinburgh working with Chris Heunen and Perdita Stevens. He is interested in applied category theory, especially applications of category theory to computer science.
Deep Learning (Partly) Demystified
Vladik Kreinovich (University of Texas at El Paso)Thursday 21 December 2023 at 10:30, room Philippe Flajolet
Invited by the Cosynus team.
Successes of deep learning are partly due to appropriate selection of activation function, pooling functions, etc. Most of these choices have been made based on empirical comparison and heuristic ideas. In this talk, we show that many of these choices – and the surprising success of deep learning in the first place – can be explained by reasonably simple and natural mathematics.
Vladik Kreinovich is Professor of Computer Science at the University of Texas at El Paso. His main interests are representation and processing of uncertainty, especially interval computations and intelligent control. He has published 13 books, 44 edited books, and more than 2,000 papers. He is President-Elect of the International Fuzzy Systems Association (IFSA), Vice President of the European Society for Fuzzy Logic and Technology (EUSFLAT), Fellow of International Fuzzy Systems Association (IFSA), Fellow of Mexican Society for Artificial Intelligence (SMIA), Fellow of the Russian Association for Fuzzy Systems and Soft Computing.
Towards a certified proof assistant kernel – What it takes and what we have
Meven Lennon-Bertrand (University of Cambridge)Tuesday 12 December 2023 at 11:00, room Nicolaas Govert de Bruijn (salle 34, rez-de-chaussée)
Invited by the Partout team.
Proof assistant kernels are a natural target for program certification: they are small, critical, and well-specified. Still, despite the maturity of the field of software certification, we are yet to see a certified Agda, Coq or Lean. In this talk, I will try and explain why this is not such an easy task, and present two complementary projects going in that direction. The first, MetaCoq, is a large scale project, broadly aiming at giving tools to manipulate Coq terms and derivations inside of Coq, in particular developing an important body of formalized proofs around Coq’s typing. The second is a more recent endeavour, aimed at tackling the mother of all properties: normalisation.
Meven Lennon-Bertrand is a post-doctoral researcher in computer science, in the CLASH group at the University of Cambridge. Previously he was a PhD student at Inria/University of Nantes in the Gallinette team, under the supervision of Nicolas Tabareau. His main interests are type theory and proofs assistants, in particular Coq. He is also quite fond of everything revolving around bidirectional typing.
Why are proofs relevant in proof relevant models?
Federico Olimpieri (University of Leeds)Wednesday 6 December 2023 at 15:00, room Philippe Flajolet
Invited by the Partout team.
Relational models of λ-calculus can be presented as type systems, the relational interpretation of a λ-term being given by the set of its typings. Within a distributors-induced bicategorical semantics generalizing the relational one, we identify the class of ‘categorified’ graph models and show that they can be presented as type systems as well. We prove that all the models living in this class satisfy an Approximation Theorem stating that the interpretation of a program corresponds to the filtered colimit of the denotations of its approximants. As in the relational case, the quantitative nature of our models allows to prove this property via a simple induction, rather than using impredicative techniques. Unlike relational models, our 2-dimensional graph models are also proof-relevant in the sense that the interpretation of a λ-term does not contain only its typings, but the whole type derivations. The additional information carried by a type derivation permits to reconstruct an approximant having the same type in the same environment. From this, we obtain the characterization of the theory induced by the categorified graph models as a simple corollary of the Approximation Theorem: two λ-terms have isomorphic interpretations exactly when their B’ohm trees coincide.
Federico Olimpieri is a postdoctoral researcher at the School of Mathematics of the University of Leeds, within the project Syntax and Semantics of 2-Dimensional Type Theory. Previously he was a PhD student between Marseille and Rome, supervised by Lionel Vaux, Laurent Regnier and Lorenzo Tortora de Falco. His research interests gravitate around the Curry-Howard-Lambek correspondence. Mainly: linear logic, lambda calculus, category theory, semantics of programming languages, type theory.
The origins of blockchains: milestones of cryptography, distributed systems and databases
Sergio Rajsbaum (Universidad Nacional Autonoma de Mexico (UNAM))Thursday 30 November 2023 at 11:30, room Amphi Sophie Germain, Batiment Turing
Invited by the COSYNUS team.
Blockchains have served as decentralized platforms to transform the way we think about databases, distributed systems and finance in a world where people can interact without knowing each other and across borders without government intermediaries. Nevertheless, an historic perspective of the ideas that brought us here can be traced back to the birth of decentralized systems in the 1970s with roots coming from research in cryptography, distributed systems and databases. A fascinating history where new notions were invented along the way, requiring the design of new algorithms, and the understanding of scientific principles about what can and cannot be done by a collection of computers communicating with each other.
Linear Hybrid Systems are Hard: The Case of Linear Complementarity Systems and The Quest For Characterizing Q-matrices
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 Q-matrix when a solution exists for all q. We start by exposing the inherent difficulty of characterizing Q-matrices by reformulating the problem as a covering problem of Rⁿ. 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 Q-matrices 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 (Lab-STICC)Friday 10 November 2023 at 14:00, room Grace Hopper
Invited by the Cosynus team.
In this talk, we provide an interval-based 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.
Holes in Monoidal and Premonoidal Categories
James Hefford (Inria Saclay, QUACS team)Monday 30 October 2023 at 11:00, room Grace Hopper
Invited by the PARTOUT team.
The category of holes or “optics” in monoidal categories dates back to the work of Pastro and Street who built on the study of profunctors with strength due to Tambara. These optics have come to be understood as a unifying language for describing various bidirectional data accessors. In this talk I will discuss the sequential and parallel composition of optics and how this can be seen to arise from a produoidal structure on the category of optics. This was first noticed by Garner and López Franco but seems often to have been neglected in applications.
Optics have also been considered over actegories - categories equipped with an action by a monoidal category - giving rise to “mixed” optics. Premonoidal categories are a particularly interesting case of actegories since they often arise in the modelling of computational side-effects. I will discuss the structure of optics over a premonoidal base and the sequential and parallel composition of such optics. In particular, one of the monoidal-like structures of this category requires a generalisation of premonoidal categories to their non-representable cousins, analogous to the generalisation from monoidal to promonoidal categories.
This talk is based on joint work with Mario Román and Matt Earnshaw.
James Hefford is an Inria postdoctoral researcher in the Quacs group at LMF. His interests include category theory and the application of these methods to problems in physics, particularly quantum theory and models of spacetime.
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 self-contained 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 (multi-dimensional) 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 multi-agent 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 16 October 2023 at 11:00, room Marcel-Paul Schützenberger
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 first-order 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) non-normalizable definitions.
Gabriel Scherer is an Inria researcher at LIX.
Mechanizing Session-Types 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) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session typed systems.
Following this approach, we mechanize a session-typed 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 session-typed 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 well-known 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 Urbana-Champaign)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 well-known 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 state-of-the-art reachability and simulation-based 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, Urbana-Champaign. 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 data-driven verification and synthesis, some of which are being commercialized. His textbook on the verification of cyber-physical 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 delta-undecidability, i.e. when properties are either true or delta-far 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, user-friendly, 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 decision-making processes. These results offer novel means for effectively integrating physics-based, contextual, or structural prior knowledge into data-driven 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 non-contractible matrix factorization of f (to be defined in the talk). Matrix factorisations are organised into a bicategory where composition is defined via a two-step 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 cut-elimination? By considering simple cases, Daniel Murfet and myself have uncovered two models of multiplicative linear logic, one in the space of coordinate rings where cut-elimination corresponds to the celebrated Buchberger Algorithm, and the other in the space of Quantum Error Correction Codes, where cut-elimination 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é Paris-Est Créteil / Université Paris-Saclay)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 non-determinism is, in some categorical sense, a particular case of the general definition. We did it on the concrete example of non-deterministic Lindenmeyer systems, and showed how the 2-monad 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
Carl-Fredrik 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. Language-theoretic methods can be used to study it, which has revealed deeps links in group theory between accessible groups, virtually free groups, the geometry of context-free graphs, and context-free languages. In this talk, I will go over some recent progress on how I have developed these methods and results to semigroup theory, as well as new techniques I developed in order to reduce such problems to problems about groups. This includes results from the theory of string rewriting systems, and a non-constructive – but highly algebraic – definition of the class of all context-free languages (or indeed the class of ET0L languages, indexed languages, etc.) via monadic rewriting systems.
Polarized Linear Logic with Fixpoints
Farzad Jafarrahmani (Laboratoire d'Informatique de Paris 6 (LIP6))Wednesday 29 March 2023 at 14:00, room Philippe 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 lambda-calculus and of system L in the style of Curien, Herbelin and Munch-Maccagnoni. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on the notion of non-uniform totality spaces and the notion of categorical model for linear logic with fixpoint. At the end, I will show you an adequacy result for μLLP between these operational and denotational semantics, from which we derive a normalization property for μLLP thanks to the properties of the totality interpretation.
On the External Validity of Average-Case Analyses of Graph Algorithms
Philipp Fischbeck (Hasso Plattner Institute, University of Potsdam)Thursday 16 March 2023 at 10:30, room Salle Emmy Noether
Invited by the ALCO team.
The number one criticism of average-case analysis is that we do not actually know the probability distribution of real-world inputs. Thus, analyzing an algorithm on some random model has no implications for practical performance. At its core, this criticism doubts the existence of external validity, i.e., it assumes that algorithmic behavior on the somewhat simple and clean models does not translate beyond the models to practical performance real-world input. With this paper, we provide a first step towards studying the question of external validity systematically. To this end, we evaluate the performance of six graph algorithms on a collection of 2745 sparse real-world networks depending on two properties; the heterogeneity (variance in the degree distribution) and locality (tendency of edges to connect vertices that are already close). We compare this with the performance on generated networks with varying locality and heterogeneity. We find that the performance in the idealized setting of network models translates surprisingly well to real-world networks. Moreover, heterogeneity and locality appear to be the core properties impacting the performance of many graph algorithms.
Perfect matchings, quantum computing and monoidal categories
Titouan Carette (University of Latvia)Thursday 9 March 2023 at 10:30, room Salle Grace Hopper
Invited by the ALCO team.
In 2002, Leslie Valiant designed a computational model based on counting the number of perfect matchings of weighted graphs: the matchgates. Matchgates can directly be interpreted as quantum processes providing an original combinatorial approach to quantum computing. In the general case, counting perfect matchings is #P-complete. However, in the specific case of planar graphs, the FKT-algorithm allows counting perfect matchings in polynomial time. As a consequence, planar matchgates provide a class of quantum computation that can be classically simulated in polynomial time.Completely independently, in 2010, as a part of the categorical quantum mechanics program, Coecke and Kissinger introduced the ZW-calculus, a graphical language inspired by two kinds of entanglement, the GHZ-states and W-states. This calculus quickly demonstrated interesting algebraic properties allowing it to be the first graphical language to be proven universal and complete for all linear maps. In this talk, I will present joint works with Étienne Moutot, Thomas Perez and Renaud Vilmart, building a bridge between the two formalisms: matchgates and ZW-calculus. It appears that reformulating matchgate theory into the category-theoretic framework of ZW-calculus allows for a much simpler presentation. Conversely, the matchgate approach provides the ZW-calculus with a straightforward combinatorial interpretation. I will introduce a fragment of ZW-calculus, the planar W-calculus, and show that it is universal and complete for matchgates. Then I will present a variety of consequences, from new algorithms for perfect matching counting and quantum simulation to a diagrammatical approach to determinant theory.
Generic pattern unification: a categorical approach
Ambroise Lafont (Cambridge)Monday 9 January 2023 at 14:00, online seminar
Invited by the PARTOUT team.
We provide a generic categorical setting for Miller’s pattern unification. The syntax with metavariables is generated by a free monad applied to finite coproducts of representable functors; the most general unifier is computed as a coequaliser in the associated multisorted Lawvere theory. Our setting handles simply-typed second-order syntax, linear syntax, or (intrinsic) polymorphic syntax such as system F.
Two-Dimensional Drift Analysis: Optimizing Two Functions Simultaneously Can Be Hard
Duri Andrea Janett (LIX)Thursday 5 January 2023 at 11:00, room Salle Philippe Flajolet
Invited by the ALCO team.
The performance of Evolutionary Algorithms (EAs) in dynamic environments, that is, environments in which the fitness function changes over time, has recently been studied (e.g., [Lengler, Meier, 2020]). In this talk, we develop and analyse a minimal example TwoLinear of a dynamic environment that can be hard for EAs. The environment consists of two linear functions f1 and f2 with positive weights 1 and n, and in each generation selection is based on one of them at random. They only differ in the set of positions that have weight 1 and n. We show that the (1+1)-EA with mutation rate χ/n is efficient for small χ on TwoLinear, but does not find the shared optimum in polynomial time for large χ.To obtain the above result, we apply drift analysis in two dimensions. Drift analysis is one of the most powerful techniques to analyse the performance and behaviour of EAs. Previously, it has only been applied in one dimension. Here, we are in the case of two random variables X1, X2, and the drift is approximatively given by A·(X1, X2)T for a matrix A. More precisely, we are in the case where X1 and X2 impede each other’s progress, and we give a full characterisation of this case.
A positive perspective on term representation
Dale Miller (LIX)Monday 5 December 2022 at 14:00, online seminar
Invited by the PARTOUT team.
Structural proof theory provides principles for organizing syntax. Many researchers have used the theory of proofs developed by Gentzen and Prawitz to design both the representation of and operations on terms. In this talk, we illustrate this tight connection between proofs and terms by using the structure of proofs in the focused proof system LJF to design term structures. Since the proof theory of LJF does not determine a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible. Such a representation of terms provides an explicit method for sharing term structures. In this setting, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to encoding untyped lambda-terms. We also exploit concurrency theory techniques—traces and simulation—to compare untyped lambda-terms using different structuring disciplines. [This is joint work with Jui-Hsuan Wu and is based on a paper that will appear in CSL 2023.]
Reasonable Space and the Lambda Calculus
Beniamino Accattoli (LIX)Monday 28 November 2022 at 14:00, online seminar
Invited by the PARTOUT team.
The lambda calculus is an expressive mathematical formalism that elegantly captures the core of functional programming languages. The evaluation of programs is modeled as a symbolic rewriting system far from low-level implementative details. This aspect has the drawback that it is not clear how to measure the time and space complexity of functional programs in a reasonable way, that is, in a way that agrees with standard computational complexity. The talk focuses on reasonable space for the lambda calculus, about which—until very recently—almost nothing was known. The talk shall survey recent results in collaboration with Ugo Dal Lago and Gabriele Vanoni (appeared in POPL 2021, LICS 2021, LICS 2022, and ICFP 2022) which have clarified the topic, and led to the first reasonable space cost model for the lambda calculus able to account for logarithmic space.
Copying and Movement, in Substructural Logics, for Natural Language Reasoning
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
Hsien-Kuei Hwang (LIX)Wednesday 9 November 2022 at 11:00, room Grace Hopper
Invited by the Alco team.
We examine and clarify in detail the contributions of Yoshisuke Matsunaga (1694?–1744) to the computation of Bell numbers in the eighteenth century (in the Edo period), providing modern perspectives to some unknown materials that are by far the earliest in the history of Bell numbers. Later clarification and developments by Yoriyuki Arima (1714–1783), and several new results such as the asymptotic distributions (notably the corresponding local limit theorems) of a few closely related sequences are also given.
Looking inside the modalities: subatomic proof theory for modal logics
Marianela Morales (LIX)Monday 7 November 2022 at 14:00, online seminar
Invited by the PARTOUT team.
There are many different cut-elimination techniques in the deep inference literature, exploiting different aspects of the proof systems they work on. A particular methodology does however stand out for its generality: cut-elimination via splitting. Even though this proof has to be redone for every proof system anew, there is a certain repeating pattern. In order to formalize this pattern and to obtain a general cut-elimination method that works for many proof systems at the same time, the method of subatomic proof theory has been developed. The basic idea is to treat atoms as binary connectives, leading to a uniform shape of all inference rules. In our work in progress we extend this idea to classical modal logics. This means that also the unary modalities are treated like binary connectives. We show soundness and completeness of the subatomic system, and we show cut-elimination via splitting for the linear fragment of the system.
Distributing and trusting proof checking
Farah Al Wardani (LIX)Monday 24 October 2022 at 14:00, online seminar
Invited by the PARTOUT team.
When a proof-checking kernel completes the checking of a formal proof, that kernel asserts that a specific formula follows from a collection of lemmas within a given logic. We describe a framework in which such an assertion can be made globally so that any other proof assistant willing to trust that kernel can use that assertion without rechecking (or even understanding) the formal proof associated with that assertion. In this framework, we propose to move beyond autarkic proof checkers—i.e., self-sufficient provers that trust proofs only when they are checked by their kernel—to an explicitly non-autarkic setting. This framework must, of course, explicitly track which agents (proof checkers and their operators) are being trusted when a trusting proof checker makes its assertions. We describe how we have integrated this framework into a particular theorem prover while making minor changes to how the prover inputs and outputs text files. This framework has been implemented using off-the-shelf web-based technologies, such as JSON, IPFS, IPLD, and public key cryptography.
Verification of cyber-physical systems: a counterexample-guided approach
Guillaume Berger (LIX)Thursday 20 October 2022 at 09:00, room Henri Poincaré
Invited by the Cosynus team.
We study counterexample-guided methods to compute stability and safety certificates for hybrid linear systems. Counterexample-guided methods involve interactions between a learner that produces candidate certificates and an oracle that verifies whether a given candidate certificate is valid. We consider two templates of polyhedral certificates: a fixed-complexity and an adaptive-complexity template. In the fixed-complexity template, the number of linear pieces of the certificate is fixed; while in the adaptive-complexity template, the number of linear pieces is updated during the learning process. For both approaches, we discuss the advantages and disadvantages, and we provide algorithmic frameworks for the computation of a certificate. Finally, we discuss current work involving extensions to correct-by-design controller synthesis.Guillaume Berger is a postdoctoral researcher in the Programming Language Verification (PLV) lab at CU Boulder, in the team of Sriram Sankaranarayanan. He received his PhD. in Mathematical Engineering from UCLouvain, Belgium, in 2021. His research focuses on automatic techniques for verification and design of complex modern systems, like cyber-physical systems, networked systems and hybrid systems.
Totalization of Ordinary Differential Equations
Riccardo Gozzi (LIX)Wednesday 19 October 2022 at 11:00, room Grace Hopper
Invited by the AlCo team.
“The totalization process was introduced by Denjoy in 1912 as an interative procedure to obtain the antiderivative of any derivative. This idea has generated the notion of Denjoy integral, first of a serie of notions of integration proposed in literature as alternatives to Riemann and Lebesgue integrals in order to successfully retrieve the antiderivative of some class of pathological derivatives. This talk follows the path taken by Denjoy, describing the details of its solution for the problem of integration, and applies it to the realm of first order ODEs, exploring the set theoretical complexity of obtaining the solution of the dynamical system for ODEs with specific pathological right-hand terms.”
A type theory for formal category theory
Max S. New (University of Michigan (MPLSE))Monday 17 October 2022 at 14:00, online seminar
Invited by the PARTOUT team.
We present a type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. By restricting the type theory to an ordered linear variant of predicate logic, we guarantee that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proof necessary. Important category theoretic proofs such as the Yoneda lemma become simple type theoretic proofs about the relationship between unit, tensor and function types, and can be seen to be ordered refinements of familiar theorems in predicate logic. The type theory comes with a sound and complete notion of categorical model based on virtual equipments, a known setting for formal category theory that has been shown to model internal, enriched and indexed category theory. This means that while the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensures that all proofs and constructions carry over to these generalized settings as well.
Accelerated Information Dissemination on Networks with Local and Global Edges
Martin Krejca (LIX)Thursday 13 October 2022 at 11:30, room Nicolaas Govert de Bruijn
Invited by the AlCo team.
“Bootstrap percolation is a classical model for the spread of information in a network. In the round-based version, nodes of an undirected graph become active once at least r neighbors were active in the previous round. We consider a slightly modified variant, acting on graphs that contain two types of edges—modeling local and global interactions, respectively. In this model, information spreads immediately via local edges but still requires a certain number r of active neighbors in order to spread via global edges. We show for certain graph classes that this modified process, when starting with a single active node, results in a phase transition with respect to how quickly further nodes are activated. Initially, the spread is rather slow, but it gains significant speed once global edges are being used to activate nodes.”
Crossover for Cardinality-Constrained Optimization
Simon Wietheger (Hasso Plattner Institute)Friday 7 October 2022 at 11:30, room Poincaré
Invited by the AlCo team.
“In order to understand better how and why crossover can benefit optimization, we consider pseudo-Boolean functions with an upper bound 𝐵 on the number of 1s allowed in the bit string (cardinality constraint). We consider the natural translation of the OneMax test function, a linear function where 𝐵 bits have a weight of 1 + 𝜀 and the remaining bits have a weight of 1. The literature gives a bound of Θ(𝑛^2) for the (1+1) EA on this function. Part of the difficulty when optimizing this problem lies in having to improve individuals meeting the cardinality constraint by flipping both a 1 and a 0. The experimental literature proposes balanced operators, preserving the number of 1s, as a remedy. We show that a balanced mutation operator optimizes the problem in 𝑂 (𝑛 log 𝑛) if,𝑛 − 𝐵 = 𝑂 (1). However, if 𝑛 − 𝐵 = Θ(𝑛), we show a bound of Ω(𝑛^2), just as classic bit flip mutation. Crossover and a simple island model gives 𝑂 (𝑛^2/log 𝑛) (uniform crossover) and 𝑂 (𝑛√𝑛) (3-ary majority vote crossover). For balanced uniform crossover with Hamming distance maximization for diversity we show a bound of 𝑂 (𝑛 log 𝑛).”
Combinatorial Flows as Bicolored Atomic Flows
Giti Omidvar (LIX)Monday 5 September 2022 at 14:00, online seminar
Invited by the PARTOUT team.
We introduce a new graphical representation of proofs which we call combinatorial flows. They can be seen as a generalization of atomic flows on one side and of combinatorial proofs on the other side. They inherit the close correspondence with open deduction and the possibility of tracing atom occurrences from atomic flows, introduced by Guglielmi and Gundersen. The correctness criterion, on the other hand, is inherited from combinatorial proofs, introduced by Hughes. Hence, combinatorial flows form a proof system in the sense of Cook and Rackhow. In this talk, I will show how to translate an open deduction derivation to a combinatorial flow. Moreover, I will introduce a normalization process for combinatorial flows with units.
A positive perspective on term representation
Jui-Hsuan Wu (Ray) (LIX)Monday 27 June 2022 at 14:00, online seminar
Invited by the PARTOUT team.
The structure of terms and expressions are represented variously via, say, labeled trees or directed acyclic graphs (DAGs). When such expressions contain bindings, additional devices are needed. In this talk, I will present the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative bias, LJF proofs encode term structures as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive bias, LJF proofs yield a structure in which explicit sharing of term structures is possible. In this situation, cut elimination yields a different notion of substitution. To illustrate these two approaches to term representation, I will give an example by applying them to the encoding of untyped λ-terms.
Analog characterization of complexity classee
Riccardo Gozzi (LIX)Tuesday 21 June 2022 at 11:00, room Grace Hopper
Invited by the AlCo team.
In the first part of the presentation I will introduce the concept of analog computation in relation with integrator devices used in the 1940’s to compute simple operations, called differntial analyzers. A description of the theoretical model behind the behaviors of those machine was first provided by Shannon, with his GPAC model which stands for Generable Purpose Analog Computation model. I will describe some of the main modifications that have been later applied in litterature to the model in order to simplify its formulation and improve its computational power. Following this guideline, I will then explain how these modifications led to an equivalence between this model and the setting of computable analysis, meaning that every function that can be computed within the computable analysis framework can also be computed by the GPAC model, and viceversa. During the course of this first, introductory, part of the talk, the motivations at the core of this research will be discussed as well. In the second part of the presentation I will illustrate how, with the correct improvements to the notion of computation of the GPAC model, this particular equivalence can be extended to the case of polynomial time complexity, leading to an equivalence between the well known complexity calss P and a certain class of systems of ODEs. To obtain this result it is required a way to encode and reproduce the behavior of the transiction function of a Turing machine in a continuous setting, keeping bounded the error introduced during this simulation.This second part of the talk will be more quantitative than the first, including more technical details. Finally, in the last part of the presentation, I will briefly mention how the results previuosly showed can be applied to further characterize higher complexity classes, such as EXPTIME or PSPACE, with similar dynamical system.
A First Runtime Analysis of the NSGA-II on a Multimodal Problem
Zhongdi QU (LIX)Tuesday 21 June 2022 at 14:00, room Philippe Flajolet
Invited by the AlCo team.
Very recently, the first mathematical runtime analyses of the multi-objective evolutionary optimizer NSGA-II have been conducted (AAAI 2022, GECCO 2022 (to appear), arxiv 2022). We continue this line of research with a first runtime analysis of this algorithm on a benchmark problem consisting of two multimodal objectives. We prove that if the population size $N$ is at least four times the size of the Pareto front, then the NSGA-II with four different ways to select parents and bit-wise mutation optimizes the OneJumpZeroJump benchmark with jump size $2 \le k \le n/4$ in time $O(N n^k)$. When using fast mutation, a recently proposed heavy-tailed mutation operator, this guarantee improves by a factor of $k^{\Omega(k)}$. Overall, this work shows that the NSGA-II copes with the local optima of the OneJumpZeroJump problem at least as well as the global SEMO algorithm.
Investigating lenses between preordered sets
Bryce Clarke (LIX)Monday 20 June 2022 at 14:00, online seminar
Invited by the PARTOUT team.
Bidirectional transformations are a means of maintaining consistency between a pair of systems. In 2005, the mathematical structure of a lens was introduced to model bidirectional transformations, and has since grown into an active topic of research in computer science and applied category theory. Classically, a system may be modelled by its set of possible states, leading to a particular notion of lens, however as more sophisticated models of systems have developed, more interesting and useful notions of lens have arisen.
The aim of this talk is to investigate lenses between preordered sets. The principal idea is that a system is modelled by its set of states equipped with a preorder, which specifies when one state may transition to another, while a lens is an order-preserving function with certain additional structure. Throughout the talk we will explore answers to several natural questions regarding the mathematical structure of lenses. How do lenses compose and decompose, both sequentially and in parallel? What are the ways in which we can build new lenses with nice properties? Given an order-preserving function, how many lens structures does it admit, and is it possible to freely generate a lens structure from it? The talk will focus on demonstrating answers to these questions via small “toy” examples, and aims to be accessible without prior knowledge of category theory. If time allows, I will discuss how the framework of lenses may be extended when systems are instead modelled by generalised metric spaces or weighted categories.
Interactive Deep Reasoning
Pablo Donato (Ecole Polytechnique Paris)Monday 30 May 2022 at 14:00, online seminar
Invited by the PARTOUT team.
In this talk, I will present the work I have been doing for my thesis in the past year and a half, which is an exploration in how to build formal proofs interactively through graphical, deep inference proof systems.
I will start with a demonstration of Actema, a prototype of graphical user interface for theorem proving in intuitionistic FOL based on direct manipulation of the proof state. A notable feature is the ability to reason by drag-and-dropping formulas within a sequent, which is a direct application of the subformula linking paradigm of K. Chaudhuri. The specificity of our approach lies in how we handle quantifiers through unification, as well as equalities. This enables both an elegant characterization, and a wide generalization of the behavior of standard rewrite tactics.
In the second part, I will present the “Bubble Calculus”, a new kind of nested sequent system which comes equipped with a nice graphical syntax. Inspired by the membranes of the Chemical Abstract Machine of Boudol and Berry, we add a so-called “bubble” construct for localizing interactions between propositions, which can be understood as internalizing the notion of premiss/subgoal inside judgments. By allowing bubbles to be polarized, one can then recover intuitionistic, dual-intuitionistic, bi-intuitionistic and classical logic as fragments which differ only in the allowed switch/membrane traversal rules.
In the third and last part, I will introduce an intuitionistic variant of the existential graphs of C. S. Peirce, arguably the first graphical proof system in the western logic tradition. To make the notation more readable, I will use a botanical metaphor where the graphs are represented as (nested) flowers. Contrarily to bubbles, flowers have a linear translation to and from traditional formulas, which allows to get completely rid of the latter in the proof system.
The Functional Machine Calculus
Willem Heijltjes (University of Bath)Monday 23 May 2022 at 14:00, online seminar
Invited by the PARTOUT team.
I will present the Functional Machine Calculus (FMC), a simple model of higher-order computation with “reader/writer” effects: state, input/output, probabilities, and non-determinism. The main result is to extend two fundamental properties of the lambda-calculus to these effects: reduction in the FMC is confluent, and a system of simple types confers strong normalization.
The premise is to view the lambda-calculus as an instruction language for a simple stack machine, in the standard way of the Krivine machine, where application is “push” and abstraction is “pop”. The FMC then consists of two independent generalizations, that are natural from the perspective of the machine.
The first generalization, “locations”, is to allow multiple stacks (or streams) on the machine, each indicated by a “location”. Application and abstraction are parameterized in these locations, to give push and pop actions on the relevant stack. Then input streams, output streams, and memory cells are straightforwardly modelled by distinct locations.
The second generalization, “sequencing”, introduces sequential composition, following the perspective of terms as sequences of machine instructions, as well as a unit, the empty sequence. This is known from Hasegawa’s kappa-calculus and from concatenative programming languages, and enables the encoding of reduction strategies, including call-by-value lambda-calculus, and for the given effects, Moggi’s metalanguage, Levy’s call-by-push-value, and Haskell Arrows.
Reduction in the FMC is confluent, which is possible because encoded effect operations reduce algebraically, rather than operationally. It can be simply typed to confer strong normalization, and because effectful operations are fully typed, it has a semantics as a Cartesian closed category. Unlike in the monadic setting, reader/writer effects in the FMC combine seemlessly.
The Skolem Landscape
Joël Ouaknine (Max Planck Institute for Software Systems, Saarbrücken, Germany)Thursday 19 May 2022 at 14:30, room Sophie Germain + online upon request (recording available)
Invited by the AlCo team.
The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, its decidability has been open for nearly a century! In this talk, I will present a survey of what is known on the Skolem Problem and related questions, including recent and ongoing developments.
Higher-order algebraic theories
Dylan McDermott (Reykjavik University)Monday 9 May 2022 at 15:30, online seminar (slides available)
Invited by the Partout team.
First-order algebraic theories describe algebraic structures that can be presented by a collection of operators and equations. These were generalized by Fiore et al. to second-order algebraic theories, in which the operators can bind simple variables. Examples include lambda-abstraction in the untyped lambda-calculus, and quantification in first-order logic.
We generalize to higher-order theories, in which operators can bind variables of higher orders. I will discuss the resulting notion of nth-order algebraic theory, and some examples. Nth-order theories have a rich metatheory, in particular they have a universal characterization as a completion, under a class of colimits, of a freely generated category. It follows from this that there is a correspondence between (n+1)th-order algebraic theories and certain monads on nth-order algebraic theories, analogous to the correspondence between (monosorted) first-order theories and finitary monads on Set.
This is joint work with Nathanael Arkor.
Neural Networks with Physics-Informed Architectures and Constraints for Dynamical Systems Modeling
Franck Djeumou (Department of Electrical and Computer Engineering at the University of Texas at Austin)Thursday 14 April 2022 at 15:00, online seminar
Invited by the AlCo team.
Effective inclusion of physics-based knowledge into deep neural network models of dynamical systems can greatly improve data efficiency and generalization. Such a priori knowledge might arise from physical principles (e.g., conservation laws) or from the system’s design (e.g., the Jacobian matrix of a robot), even if large portions of the system dynamics remain unknown. We develop a framework to learn dynamics models from trajectory data while incorporating a priori system knowledge as inductive bias. By exploiting a priori system knowledge during training, the proposed approach learns to predict the system dynamics two orders of magnitude more accurately than a baseline approach that does not include prior knowledge, given the same training dataset.
Efficient Synthesis of Controllers using Abstraction-Based Approaches
Elena Ivanova (Cosynus)Wednesday 6 April 2022 at 14:00, room Grace Hopper
Invited by the Cosynus team.
The first part of the talk will be dedicated to a control synthesis for cyber-physical systems using abstraction-based control synthesis approaches. These approaches first create a finite-state abstraction (or a symbolic model) for a continuous or hybrid system and then refine the controller synthesized for the abstraction to a controller for the original system. Abstraction-based control synthesis techniques allow us to handle complex dynamics of CPS models and non-trivial specifications (for instance given by LTL formulas) but suffer from poor scalability. I will talk about how to improve the efficiency of ABS approaches when safety specification is considered. The second part of the talk will be dedicated to ongoing research on efficient approximations of the reachable sets.
Groupe fondamental et pavages du plan: quelques constructions
Léo Paviet Salomon (Greyc, Caen)Thursday 24 March 2022 at 11:00, room Salle Henri Poincaré
Invited by the AlCo team.
On appelle sous-shift (ou sous-décalage) un ensemble de pavages ou de coloriages du plan respectant certaines contraintes locales. Historiquement introduits comme discrétisations de systèmes dynamiques continus, on se propose ici d’en étudier un invariant topologique, introduit par W.Geller et J.Propp, le Groupe Fondamental Projectif. A l’instar de la définition habituelle du groupe fondamental, un invariant d’espaces topologiques, il s’agira ici de comprendre comment l’on peut définir une notion de chemins dans les pavages, reliant les configurations entre elles, et d’étudier comment les déformations de ces chemins permettent d’associer à chaque pavage un unique objet algébrique: son groupe fondamental projectif. En particulier, on montrera dans cet exposé comment réaliser une large classe de groupes comme groupes fondamentaux de certains pavages.
Visibly pushdown languages in AC⁰
Nathan Grosshans (Universität Kassel, Germany.)Thursday 17 March 2022 at 11:00, online seminar
Invited by the AlCo team.
One important research endeavour at the intersection of circuit complexity theory, algebraic automata theory and logic is the classification of regular languages according to their localisation within the internal structure of NC¹, the class of languages decided by Boolean circuits of polynomial size, logarithmic depth and with gates of constant fan-in. In some sense, the search for such a classification concentrates most of the open questions we have about the relationship between NC1 and its well-studied subclasses.
While many questions are still open, one of the greatest successes of this research endeavour has been the characterisation of the regular languages in AC⁰, the subclass of NC¹ corresponding to Boolean circuits of polynomial length, constant depth and with gates of unbounded fan-in. This characterisation takes the form of a triple languages-algebra-logic correspondence: a regular language is in AC0 if and only if its syntactic morphism is quasi-aperiodic if and only if it is definable in first-order logic over words with linear order and modular predicates.
It is natural to try to extend such results to classes of formal languages greater than the class of regular languages. A well studied and robust such class is given by visibly pushdown languages (VPLs): languages recognised by pushdown automata where the stack-height-behaviour only depends on the letters read from the input. Over the previous decade, a series of works concentrated on the fine complexity of VPLs, with several achievements: one of those was a characterisation of the class of visibly counter languages (basically VPLs recognised by visibly pushdown automata with only one stack symbol) in AC⁰ by Krebs, Lange and Ludwig. However, the characterisation of the VPLs in AC⁰ still remains open.
In this talk, I shall present a conjectural characterisation of the VPLs in AC⁰ obtained with Stefan Göller at the Universität Kassel. It is inspired by the conjectural characterisation given by Ludwig in his Ph.D. thesis as a generalisation of the characterisation for visibly counter languages, but that is actually false. In fact, we give a more precise general conjectural characterisation that builds upon recognisability by morphisms into Ext-algebras, an extension of recognisability by monoid-morphisms proposed by Czarnetzki, Krebs and Lange to suit the case of VPLs. This characterisation classifies the VPLs into three categories according to precise conditions on the Ext-algebra-morphisms that recognise them:
- those that are TC⁰-hard;
- those that are in AC⁰;
- those that correspond to a well-identified class of “intermediate languages” that we believe to be neither in AC⁰ nor TC⁰-hard.
On Equivalence and Similarity of Polymorphic Proofs and Programs
Paolo Pistone (University of Bologna)Monday 7 March 2022 at 14:00, online seminar
Invited by the Partout team.
Under the proofs-as-programs paradigm, the problem of program equivalence, that is, of understanding whether two programs compute the same function, can be related to the problem of equivalence proof, that is, of understanding whether two formal derivations represent, in some sense, the same proof. In this talk I will discuss some methods to capture program/proof equivalence in System F, the paradigmatic language for parametric polymorphism, through the definition of an invariant, for each type, called the characteristic. This invariant provides a means to know whether, in the proofs of a given formula, propositional quantification (i.e. polymorphism) is eliminable via parametricity, yielding a way to test equivalence in a finite way. Moreover, I will sketch how parametricity and related methods for equivalence can be lifted to a more quantitative setting (as those arising from probabilistic or approximate computation) in which the vital property to understand is whether two programs, albeit non-equivalent, behave in a sufficiently similar way, so that replacing the one by the other cannot alter the results of computation too much.
The Power of Probabilistic Models in Optimization
Martin Krejca (LIP 6)Thursday 17 February 2022 at 11:00, room Salle Philippe Flajolet
Invited by the AlCo team.
For many real-world optimization problems, the objective function is only indirectly accessible, for example, via simulations. In this setting, randomized search heuristics (RSHs) are applied to great success, guided solely by the quality of samples. One important class of these heuristics are estimation-of-distribution algorithms (EDAs), which maintain and refine a probabilistic model of the search space.
In this talk, I discuss some of my results on the theoretical analysis of EDAs by presenting properties of EDAs that set them apart from other RSHs. We see that EDAs cope inherently well with noisy objective functions, due to the probabilistic model tolerating faulty updates to a certain degree. However, we also show that these models typically degenerate if important updates are withheld for longer periods of time. We conclude by presenting how this problem is circumvented when applying better rules to handle updates.
Holomorphic Quantum Computing
Ulysse Chabaud (Institute for Quantum Information and Matter, Caltech, US)Thursday 3 February 2022 at 16:30, online seminar
Invited by the AlCo team.
The advent of quantum information processing promises dramatic advantages with respect to its classical counterpart, notably for computing. I will give an introduction to quantum computing through the lens of holomorphic functions, which allow us to elegantly describe both discrete- and continuous-variable quantum computations, using classical dynamical systems. As an application, I will discuss the characterisation of quantum properties that are necessary resources for quantum computational advantages, such as non-Gaussianity or entanglement.
Joint work with Saeed Merhaban (arXiv:2111.00117).
Variable binding and substitution for (nameless) dummies
Ambroise Lafont (UNSW Sydney)Monday 25 October 2021 at 14:00, room Marcel-Paul Schützenberger (recording available)
Invited by the Partout team.
[Organizer’s note: this will be a hybrid seminar, simultaneously taking place at Salle Marcel-Paul Schützenberger and on BBB.]
By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.
Joint work with Tom & Andre Hirschowitz, Marco Maggesi
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 model-checking, to SMT-based proofs. Also, they apply to various classes of programs from concurrent data types, to distributed databases, or applications thereof.
History-aware Higher Dimensional Modal Logic
Christian Johansen (Norwegian University of Science and Technology)Wednesday 7 July 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
This talk presents a modal logic over HDAs which incorporates two modalities for reasoning about “during” and “after”. This higher dimensional modal logic (HDML) is decidable and an “almost” complete axiomatic system exists for it. When the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. One can isolate the class of HDAs that encode Mazurkiewicz traces and show how HDML, with natural definitions of corresponding Until operators, can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces) or the branching time ISTL. A preliminary study of the expressiveness of the basic HDML language wrt. bisimulations has concluded that HDML captures the split-bisimulation. One can also add backward-looking modalities (i.e., past modalities) so to increase the expressiveness so to be able to capture the hereditary history-preserving bisimulation. Classical examples from the literature that are used to distinguish one-or-another bisimulation can be distinguished in this hHDML using a specially crafted formula. I will show these interesting examples and talk about the respective literature, if time permits.
Greibach Normal Form and Simple Automata for Weighted ω-Context-Free Languages
Sven Dziadek (Universität Leipzig)Wednesday 30 June 2021 at 11:00, online seminar
Invited by the Cosynus team.
In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of ω-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted context-free languages, or ω-algebraic series, can be represented as solutions of (mixed) ω-algebraic systems of equations and by weighted ω-pushdown automata.
In our first main result, we show that (mixed) ω-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple ω-reset pushdown automata recognize all ω-algebraic series. Simple ω-reset automata do not use ε-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted context-free languages.
This talk is based on this article and its corresponding short version.
Distributed Denial of Service cyber-attacks in 5G networks: a robust approximation approach
Sonia Vanier (Délégation au LIX, et Université Paris, Panthéon-Sorbonne)Thursday 24 June 2021 at 14:30, online seminar
Invited by the AlCo team.
Distributed Denial of Service (DDoS) cyberattacks represent a major security risk for network operators and internet service providers. They thus need to invest in security solutions to protect their network against DDoS attacks. The present work focuses on deploying a network function virtualization based architecture to secure a network against an on-going DDoS attack. We assume that the target, sources and volume of the attack have been identified. However, due e.g. to 5G network slicing, the exact routing of the illegitimate flow in the network is not known by the internet service provider. We seek to determine the optimal number and locations of virtual network functions in order to remove all the illegitimate traffic while minimizing the total cost of the activated virtual network functions. We propose a robust optimization framework to solve this problem. The uncertain input parameters correspond to the amount of illegitimate flow on each path connecting an attack source to the target and can take values within a predefined uncertainty set. In order to solve this robust optimization problem, we develop an adversarial approach in which the adversarial sub-problem is solved by a Branch & Price algorithm. The results of our computational experiments, carried out on medium-size randomly generated instances, show that the proposed solution approach is able to provide optimal solutions within short computation times
Client-Server Sessions in Linear Logic
Alex Kavvos (Bristol)Wednesday 23 June 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.
We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of weakening and contraction. This makes them a suitable logical device for encapsulating the pattern of a server receiving requests from an arbitrary number of clients on a single channel. Guided by this intuition we formulate a system of session types based on Classical Linear Logic with coexponentials, which is suited to modelling client-server interactions. We also present a session-typed functional programming language for client-server programming, which we translate to our system of coexponentials.
Tracks in Higher Dimensional Automata
Krzysztof Ziemiański (University of Warsaw)Wednesday 23 June 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
The main goal of my talk is to present two models of executions of Higher Dimensional Automata. A track in a HDA is a sequence of cells such that every cell is either an upper face or an upper coface of the preceding one. To every track we can assign the (evi)pomset of its events; it is a labeled interval order equipped with an additional secondary ordering. Then we consider the set of tracks between fixed source and target cells, up to certain equivalence. This set is naturally a presheaf over the category of evipomsets, which is our first model of executions of HDA. This model can be simplified. When we restrict to step-sequence executions, ie, tracks in which the consecutive cells have only one common vertex, we obtain a presheaf over permutahedral category. This model is combinatorially simpler. At first glance it seems too restrictive but there is some evidence that this is not the case: the space of topological executions is homotopy equivalent to the geometric realization of the permutahedral model.
Intersection type distributors
Federico Olimpieri (LIPN)Monday 7 June 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.
We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.
On Monadic Rewriting Systems
Francesco Gavazzo (University of Bologna)Wednesday 19 May 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
Motivated by the study of effectful programming languages and computations, I will introduce the theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, effects being modelled as monads. Such systems are to effectful computations and programming languages what traditional rewriting systems are to pure computations and programming languages. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining mathematically and operationally meaningful notions of monadic rewriting turns out to be simply not possible for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible.
I will answer that question by showing that the so-called weakly cartesian monads precisely describe computational effects for which monadic rewriting is well-behaved. If monads are given as equational theories, as it is in the case of algebraic effects, a sufficient condition ensuring monadic rewriting to be well-behaved can be given by looking at the shape of the theory only: such a condition dates back to an old theory by Guatam and requires equations to be linear. Finally, I will apply the abstract theory of monadic rewriting systems to the call-by-value λ-calculus with algebraic effects, this way obtaining the extension of the well-known confluence and standardisation theorems to an effectful setting.
Analog characterization of standard complexity classes by means of ODEs
Riccardo Gozzi (Instituto Superior Técnico, Portugal)Wednesday 12 May 2021 at 10:30, online seminar
Invited by the AlCo team.
In this presentation it will be shown how to make use of ordinary differential equations (ODEs) to describe standard complexity classes. Previously it was shown that the classes P and FP can be characterized with ODEs. Here we show that ODEs can also be used to characterize a wide range of computable functions, from exponentials up to including all elementary functions. It will be also discussed the case of space complexity classes, introducing the definition of a particular dynamical system able to describe functions in FPSPACE. Finally, to complement what have been done with functions, the treatment of classes of languages such as EXPTIME and PSPACE will be included in the analysis.
Verifying Hybrid Systems with Interactive Theorem Provers
Georg Struth (University of Sheffield)Wednesday 21 April 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
Hybrid systems integrate continuous dynamics and discrete control. A prominent approach is differential dynamic logic (dL), a modal logic for reasoning about ordinary differential equations and their solutions within hybrid programs. Over the last decade, a domain-specific sequent calculus for dL has been developed together with an intricate explicit substitution calculus for it. It has been integrated into the KeYmaera X tool and proved its worth in numerous case studies.
This talk presents an algebraic reconstruction of this approach and the first verification and refinement components in an interactive proof assistant inspired by it. Our components are based on shallow embeddings in which the proof theory of dL is by and large replaced by semantic equational reasoning about orbits and trajectories of dynamical systems in combination with discrete state updates. We use algebras, in particular variants of Kleene algebras and predicate transformer algebras, for automatic verification condition generation. We currently support a component for reasoning with weakest liberal preconditions, a Hoare logic and a refinement calculus for hybrid programs.
These allow us to verify hybrid programs in various ways: starting from hybrid program specifications based on ordinary differential equations, we can certify solutions of locally Lipschitz-continuous vector fields using the Picard-Lindelöf theorem and then reason explicitly about them. Alternatively we can represent solutions of continuous vector fields implicitly by invariant sets. Finally, we can analyse hybrid program that specify trajectories or orbits of hybrid systems directly.
Apart from presenting the algebras used and their extension and instantiation to hybrid program semantics, I will present some examples, comment on the intricacies of formalising the approach within the Isabelle/HOL proof assistant, and outline some future directions for this line of work, time permitting.
This work is joint with Jonathan Julián Huerta y Munive, and partially funded by CONACYT.
An introduction to ZX-calculus
Renaud Vilmart (LMF, ENS Paris-Saclay)Wednesday 14 April 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
The ZX-Calculus is a powerful graphical language for representing quantum processes, stemming from category theory. Its primitives are close to that of the hardware these processes will supposedly be implemented on, and yet it enjoys some level of abstraction. In particular, it is equipped with an intuitive equational theory, allowing us to relate processes that are equivalent, i.e. that represent the same quantum evolution. The plasticity and the equational theory of the language make it a particularly good candidate for unifying different models of quantum computation, for optimisation, as well as for verifying properties or equivalences of processes.
Time-Optimal Self-Stabilizing Leader Election in Population Protocols
Janna Burman (LISN, Université Paris-Saclay)Thursday 8 April 2021 at 14:30, online seminar
Invited by the AlCo team.
We consider the standard population protocol model, where (a priori) indistinguishable and anonymous agents interact in pairs according to uniformly random scheduling. The self-stabilizing leader election problem requires the protocol to converge on a single leader agent from any possible initial configuration. We initiate the study of time complexity of population protocols solving this problem in its original setting: with probability 1, in a complete communication graph. The only previously known protocol by Cai, Izumi, and Wada [Theor. Comput. Syst. 50] runs in expected parallel time Θ(n²) and has the optimal number of n states in a population of n agents. The existing protocol has the additional property that it becomes silent, i.e., the agents’ states eventually stop changing.
Observing that any silent protocol solving self-stabilizing leader election requires Ω(n) expected parallel time, we introduce a silent protocol that uses optimal O(n) parallel time and states. Without any silence constraints, we show that it is possible to solve self-stabilizing leader election in asymptotically optimal expected parallel time of O(log n), but using at least exponential states (a quasi-polynomial number of bits). All of our protocols (and also that of Cai et al.) work by solving the more difficult ranking problem: assigning agents the ranks 1, … ,n.
Une petite histoire de la K-trivialité
Benoit Monin (Université de Créteil)Thursday 1 April 2021 at 14:30, online seminar
Invited by the AlCo team.
La complexité de Kolmogorov est utilisée avec succès pour caractériser l’aléatoire pour les chaînes binaires infinies : Il s’agit des chaînes dont la complexité de Kolmogorov de leurs préfixes est maximale. A l’opposé, les chaînes binaires infinies dites “K-triviales” sont celles dont la complexité de Kolmogorov de leurs préfixes est minimale. La classe des K-triviaux est dénombrable, et contient “juste un peu plus” que les chaînes binaires infinies calculables. Les nombreuses études sur les K-triviaux depuis une vingtaine d’années ont révélé la grande richesse de cette classe. Nous en présenterons les différents aspects.
Linear Constraints
Arnaud Spiwack (Tweag)Wednesday 31 March 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.
In the past few years, I’ve been involved in extending the type system of the Haskell programming language to support linear types. In one sentence, a linear argument must be consumed exactly once in the body of its function; a linear function is a function whose argument is linear. Such a linear type system comes from linear logic (or, in this particular case, intuitionistic linear logic, but who’s counting?) seen through the lens of the Curry-Howard correspondence. Linear typing has two main families of applications: making pure interface to mutable data structures, such as arrays (“pure” means that functions are functions in the sense of mathematics); and enforcing protocol in the type level, for instance making sure file handles are eventually closed and not written to after being closed. An example that combines both aspects is safe manual memory management, much in the style that the Rust programming language allows.
This is all possible in the, latest, 9.0 release of GHC. However these applications, using GHC 9.0’s linear types require quite a bit of additional syntactic bureaucracy, compared to their unsafe equivalent. In this talk, after introducing Haskell’s linear types, I’ll present linear constraints, a front-end feature for linear typing that decreases the bureaucracy of working with linear types. Linear constraints are implicit linear arguments that are to be filled in automatically by the compiler. Linear constraints are presented as a qualified type system, together with an inference algorithm which extends OutsideIn, GHC’s existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell.
Gauge-invariance in celullar automata and multi-scales analysis
Giuseppe Di Molfetta (Aix-Marseille University)Thursday 18 March 2021 at 14:30, online seminar
Invited by the AlCo team.
Cellular Automata constitute the most established distributed model of computation on space-time grid. It is clearly physics-like, in the sense that it shares some fundamental symmetries such as homogeneity (invariance of the physical laws in time and space), causality, and often reversibility. When a CA is invariant under a transformation identically performed at every point of the configuration space, they are said to have a global symmetry. Typical global symmetries include reflections, rotations, time inversion. Local symmetries, the cornerstone of gauge theories, is a stronger constraint. I will provide a constructive method, a step-by-step procedure, to make cellular automata invariant under the local action of a gauge group and the notion of gauge-equivalence will be formalized. Then, I will extend such results into the Quantum realm by means of a concrete example. In conclusion, I will discuss how such discrete time and discrete space gauge invariant automata can be described at larger scale, e.g. by differential equations, with and without information loss.
Proof Theory of Skew Monoidal Categories
Niccolò Veltri (Tallinn University of Technology)Monday 15 March 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.
(Joint work with Tarmo Uustalu and Noam Zeilberger)
The skew monoidal categories of Szlachányi are a weakening of monoidal categories where the three structural laws of left and right unitality and associativity are not required to be isomorphisms but merely transformations in a particular direction. In this talk, we show that the free skew monoidal category on a set of generating objects can be concretely presented as a sequent calculus. This calculus enjoys cut elimination and admits focusing, i.e. a subsystem of canonical derivations, which solves the coherence problem for skew monoidal categories.
We also develop sequent calculi for partially normal skew monoidal categories, which are skew monoidal categories with one or more structural laws invertible. Each normality condition leads to additional inference rules and equations on them. We prove cut elimination and we show that the calculi admit focusing. The result is a family of sequent calculi between those of skew monoidal categories and (fully normal) monoidal categories. On the level of derivability, these define 8 weakenings of the (unit,tensor) fragment of intuitionistic non-commutative linear logic.
If time allows it, we briefly discuss the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew closed categories in turn are a weakening of the closed categories of Eilenberg and Kelly where no structural law is required to be invertible and the presence of a monoidal structure is not required.
Automated Formal Testing of Transactional Databases and Applications
Constantin Enea (IRIF)Wednesday 10 March 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and are resilient to failures. Modern databases provide different isolation levels for transactions corresponding to different tradeoffs between consistency and availability. The weaker the isolation level, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors.
I will present a series of recent results that concern the problem of testing transactional databases and database-backed applications. First, I will focus on the problem of checking whether a given execution of a transactional database adheres to some isolation level, showing that isolation levels like read committed, read atomic, and causal consistency are polynomial-time checkable while prefix consistency and snapshot isolation are NP-complete in general. These results complement a previous NP-completeness result concerning serializability. Moreover, in the context of NP-complete isolation levels, we devise algorithms that are polynomial time assuming that certain parameters in the input executions, e.g., the number of sessions, are fixed. Second, I will present MonkeyDB, a mock storage system for testing database-backed applications. MonkeyDB supports a Key-Value interface as well as SQL queries under multiple isolation levels. It uses a logical specification of the isolation level to compute, on a read operation, the set of all possible return values. MonkeyDB then returns a value randomly from this set. We show that MonkeyDB provides good coverage of weak behaviors, which is complete in the limit.
Understanding the lambda-calculus via linearity and rewriting.
Giulio Guerrieri (University of Bath)Monday 1 March 2021 at 14:00, online seminar (recording available)
Invited by the Partout team.
The lambda-calculus is the model of computation underlying functional programming languages and proof assistants. Actually, there are many lambda-calculi, depending on the evaluation mechanism (e.g., call-by-name, call-by-value, call-by-need) and computational feature that the calculus aims to model (e.g., plain functional, non-deterministic, probabilistic, infinitary).
The existence of different paradigms is troubling because one apparently needs to study the theory and semantics of each one separately.
We propose a unifying meta-theory of lambda-calculi, where the study is rooted on a unique core language, the bang calculus, a variant of the lambda-calculus inspired by linear logic: a bang operator marks which resources can be duplicated or discarded.
The bang calculus subsumes both call-by-name and call-by-value. A property studied in the bang calculus is automatically translated in the corresponding property for the call-by-name lambda-calculus and the call-by-value lambda-calculus, thanks to two different embeddings of the lambda-calculus in the bang calculus. These embeddings are grounded on a proof theory: they are an adaptation of Girard’s two translations of intuitionistic logic into linear logic.
Advanced computational features are usually obtained by adding new operators to a core language. Instead of studying the operational properties of the extended language from scratch, we propose a simple method to study them modularly: if an operational property holds in the core language and in the new operators separately, then a simple test of good interaction between core language and new operators guarantees that the property lifts to the whole extended language. This approach is first developed in abstract rewriting systems.
Mathematical specifications of programming languages via modules over monads
Ambroise Lafont (UNSW Sydney)Monday 22 February 2021 at 10:30, online seminar (recording available)
Invited by the Partout team.
Research in the field of programming languages traditionally relies on a definition of syntax modulo renaming of bound variables, with its associated operational semantics. We are interested in mathematical tools allowing us to automatically generate syntax and semantics from basic data. We pay particular attention to the notion of substitution, using the categorical notions of monads and modules over them. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets. We provide a further notion of transition monads which takes into account the operational semantics. We give examples of specifications for transition monads, in the spirit of Initial Semantics, where an object is characterized by some initiality property in a suitable category of models.
Logical Analysis of Data
Miki Hermann (LIX)Thursday 18 February 2021 at 14:30, online seminar
Invited by the AlCo team.
We show how to cope with Big Data by means of Automated Deduction. We generate a Horn or a bijunctive formula from sets of positive and negative tuples T and F, respectively These sets of tuples have been previously shortened to a locally minimal length, provided that the two sets T and F keep an empty intersection. Since the problem to find the minimal length is an NP-optimization problem, we apply different approximation strategies. We also apply two approaches to formula production: (1) the LARGE approach, where only tuples of F falsify the produced formula, and (2) EXACT, where only tuples of T satisfy the formula. In case of the large approach we apply a set cover approximation algorithm to keep the minimal set of clauses falsifying all tuples from the set F. The produced formula can be used to further characterize subsequent sets of tuples and identify their membership among the true or false examples. The whole system, called MCP for Multiple Characterization Problem, has been implemented and can be found at https://github.com/miki-hermann/mcp.
(research done in collaboration with Gernot Salzer, Technische Universität Wien, Vienna, Austria)
Generating Posets Beyond N
Uli Fahrenberg (LIX)Wednesday 17 February 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
We introduce iposets - posets with interfaces - equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem more interesting for modeling concurrent and distributed systems, can be generated, but not all posets. Generating posets is also important for constructing free algebras for concurrent semirings and Kleene algebras that allow compositional reasoning about such systems.
Gentzen-Mints-Zucker duality: sequent calculus vs λ-calculus
Daniel Murfet (University of Melbourne)Monday 8 February 2021 at 09:30, online seminar
Invited by the Partout team.
I will report on joint work with Will Troiani, in which we revisit Howard’s work on the Curry-Howard correspondence and interpret it as an isomorphism between a category of proofs in intuitionistic sequent calculus and a category of terms in simply-typed λ-calculus. Some version of this is known to the experts due to work of Mints, Zucker and others, but not for Gentzen’s original calculus. I will explain our technical contributions to the understanding of normal forms of sequent calculus proofs, and our view that the fundamental duality expressed is not between “proofs and programs” but between local and global presentations of a logico-computational structure.
Games for constructive modal logics
Matteo Acclavio (University of Luxembourg)Monday 1 February 2021 at 14:00, online seminar
Invited by the Partout team.
Constructive modal logics are extensions of intuitionistic propositional logic with certain modal axioms. Many proof systems are known for these logics, but the only available denotational semantics is defined by means of an abstract construction, based on the quotient of their lambda terms.
The general aim of our work is to define a game semantics for constructive modal logics. In this talk I will define the winning strategies for a formula and show the correspondence between winning strategies and proofs. I will show how winning strategies can be defined as the projection of specific paths in a graphical proof system defined for this purpose - combinatorial proofs.
(this talk is based on a joint work with Davide Catta and Lutz Strassburger)
A diagrammatic axiomatisation of finite-state automata
Robin Piedeleu (University College London)Wednesday 27 January 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
In this talk I will present a fully diagrammatic approach to the theory of finite-state automata, based on reinterpreting their usual state-transition graphs as string diagrams. Moreover, I will give an equational theory that completely axiomatises language equivalence in this new setting. The proposed axiomatisation is finitary— a result which is provably impossible to obtain for the usual one-dimensional syntax of regular expressions.
Abstract rewriting Internalised
Maxime Lucas (Université Sorbonne Paris Nord)Wednesday 13 January 2021 at 11:00, online seminar (recording available)
Invited by the Cosynus team.
There are two historical trends in rewriting theory: “abstract rewriting”, where one rewrites terms, and “algebraic rewriting”, where one rewrites linear combinations of terms. Although the two theories enjoy similar results, there are subtle differences that prevent the development of a unified theory: for example in algebraic rewriting any reflexive relation is both symmetric and transitive. In this talk we present a generic framework to study rewriting in a category C satisfying some suitable hypothesis. In the case C = Set we recover abstract rewriting, while algebraic rewriting corresponds to the case where C is the category of vector spaces. In this framework, we express notions of termination, confluence and local confluence using a notion of rewriting strategy, and prove an analogue of Newman’s Lemma. Finally, we hint at the higher dimensional analogue of this framework, with a view towards homotopy.