The classical statement of the Chomsky-Schützenberger representation theorem says that any context-free language may be represented as the homomorphic image of the intersection of a Dyck language of balanced parentheses with a regular language. In the talk I will discuss a fibrational perspective on context-free grammars and finite-state automata that grew out of a long-running project with Paul-André Melliès on type refinement systems, but with a surprising twist that only emerged when we considered the C-S theorem. It turns out that underlying that theorem is a basic adjunction between categories and colored operads (= multicategories), where the right adjoint $W : Cat \to Oper$ builds a “spliced arrow operad” out of any category, and the left adjoint $C : Oper \to Cat$ sends any operad to a “contour category” whose arrows have a geometric interpretation as oriented contours of operations.

Based on joint work with Paul-André Melliès that appeared at MFPS 2022 (https://hal.science/hal-03702762), as well as a long version of that article in preparation.

Joint work with Nadime Francis, Amélie Gheerbrant, Paolo Guagliardo, Leonid Libkin, Victor Marsault, Wim Martens, Filip Murlak, Liat Peterfreund and Domagoj Vrgoč The development of practical query languages for graph databases runs well ahead of the underlying theory. The ISO committee in charge of database query languages is currently developing a new standard called Graph Query Language (GQL), the main component of which is the pattern matching facility. In many aspects, it goes well beyond RPQs, CRPQs, and similar queries on which the research community has focused for years. In this talk, I will present our distillation of the lengthy standard into a simple Graph Pattern Calculus (GPC) that reflects all the key pattern matching features of GQL.

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules.

Zoom meeting registration link

YouTube live stream

Robots are facilitating new business models from food delivery to healthcare. Current engineering practice cannot yet provide the formal guarantees needed to allay the safety concerns of regulators. Simulation, a technique favoured by practitioners, provides an avenue for experimenting with different scenarios before committing to expensive tests and proofs. In this talk, I will discuss how different models may be brought together for the (co-)verification of system properties, with simulation complementing formal verification. This will be explored in the context of the model-driven RoboStar framework, that clearly identifies models of the software, hardware, and scenario, and has heterogeneous formal semantics amenable to verification using model-checkers and theorem provers.

A computer system is safety-critical when it can cause serious damage to property, the environment, human life, or to society as a whole. Real-world safety-critical systems are also necessarily complex, because, to take into account the interactions between software, hardware, the physical environment, and sometimes their distributed nature (systems of systems), they need to implement a variety of safety measures, in software, hardware, in the system design, at development time, at compile time, and at run-time. Those safety measures which vary from one safety-critical system to another very often lead to a decrease in performance, for a increase in the execution time of software.

This research work is situated in the context of one such system, the communication-based train control (CBTC) system of Siemens Mobility France which operates a number of driverless subway systems around the World, including Paris lines 1, 4, and 14. That system is certified according to the industrial norm EN-50128 and up to the highest Safety Integrity Level 4, required for safety-critical systems with potentially catastrophic consequences. In this context, the thesis looks for an answer to the question of how to automatically optimize the execution time performance of such systems without losing the previously obtained safety guarantees.

The answer provided is provably correct optimization of source code. A first contribution is a source-to-source compiler for VCP Ada (a subset of Ada) programs, that optimizes source code while preserving the formal semantics of the programs. The compiler has been proven correct in the Coq proof assistant and guarantees the equivalence of execution between the original and the optimized program. The compiler copes with the complexities of the platform, due to hardware safety measures, which is important, since real-world safety-critical systems are often susceptible to having such measures, potentially conflicting with existing formally proven optimizing compilers. Moreover, choosing the approach of a source-to-source compilation shows to have methodological advantages over an approach to proven optimizations having a number of intermediate languages, allowing to simplify and diminishing the needed proof effort.

A second contribution is to the problem of provably correct lexical analysis of compilers, which has previously not received a lot of research attention, a weak link in any compilation chain using a proven or qualified compiler. We develop CoqLex, the first Coq-formalized lexer generator, based on a modification of an existing Coq implementation of regular expression matching via Brzozowski derivatives.

The developed theory and tools have been applied to optimize real-world VCP Ada programs of CBTC systems, consisting of thousands of source files, with promising results.

The problem of undirected st-connectivity is important both for its applications in network problems, and for its theoretical connections with logspace complexity. Classically, a long line of work led to a time-space tradeoff of T=Õ(n^2/S) for any S such that S=Ω(log(n)) and S=O(n^2/m), where T is the running time and S is the used space. In this talk, I will present a surprising result that quantumly there is no nontrivial time-space tradeoff: there is a quantum algorithm that achieves both optimal time Õ(n) and optimal space O(log(n)) simultaneously. This improves on previous results, which required either O(log(n)) space and Õ(n^1.5) time, or Õ(n) space and time. To complement this, we show that there is a nontrivial time-space tradeoff when given a lower bound on the spectral gap of a corresponding random walk.

PureCake, is a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. This talk will present how optimization soundness can be proven using equational reasoning with the example of the demand analysis pass and other related optimizations.

Based on : PureCake: A Verified Compiler for a Lazy Functional Language [PLDI'23] by Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti

Previous work reduces the problem of deciding whether a weighted finite automaton (WFA) over a field is equivalent to a sequential, respectively, unambiguous, WFA to the computation of the linear hull. The linear hull is the topological closure of the reachability set in a certain linear version of the Zariski topology. We discuss an algorithm to compute the linear hull that works essentially entirely in the realm of linear algebra (i.e., without first resorting to the computation of the finer Zariski topology). Further, we show how this leads to double-exponential bounds on the size of the linear hull.

This talk is on joint work with J. Bell.