We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ω-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.

Quantum analogue simulation aims to reproduce the physics of a target Hamiltonian H, using a different physical system; and this can be achieved by ensuring that the low energy subspace of the physical Hamiltonian is approximately H. First I will describe a construction of a 1D quantum system that can simulate all other Hamiltonians (a property we call universality) just by varying the length of the chain. The construction relies heavily on the possibility of encoding a (quantum) computation into the chain. Then I will go onto show a much more general equivalence between universality and the computational complexity of the Local Hamiltonian problem - the problem of approximately estimating the ground state energy of a system.

Based on https://arxiv.org/abs/2003.13753 and https://arxiv.org/abs/2101.12319

We survey several different methods of constructing infinite graphs out of the families of finite graphs, among the Fraîssé limits, the morasses, the ultraproducts and the graphons/measurings. Concentrating on a couple of them, we talk about various colourings and the generalised Ramsey theory.

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way. While very promising, this methodology was previously not fully formalised and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalising the lower-level details, which together enable constructing fully machine-checked crypto proofs in the Coq proof assistant. Moreover, SSProve is itself formalised in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.

The Markoff injectivity conjecture states that $w\mapsto\mu(w)_{12}$ is injective on the set of Christoffel words where $\mu:\{\mathtt{0},\mathtt{1}\}^*\to\mathrm{SL}_2(\mathbb{Z})$ is a certain homomorphism and $M_{12}$ is the entry above the diagonal of a $2\times2$ matrix $M$. Recently, Leclere and Morier-Genoud (2021) proposed a $q$-analog $\mu_q$ of $\mu$ such that $\mu_{q\to1}(w)_{12}=\mu(w)_{12}$ is the Markoff number associated to the Christoffel word $w$. We show that there exists an order $<_{radix}$ on $\{\mathtt{0},\mathtt{1}\}^*$ such that for every balanced sequence $s \in \{\mathtt{0},\mathtt{1}\}^\mathbb{Z}$ and for all factors $u, v$ in the language of $s$ with $u <_{radix} v$, the difference $\mu_q(v)_{12} - \mu_q(u)_{12}$ is a nonzero polynomial of indeterminate $q$ with nonnegative integer coefficients. Therefore, for every $q>0$, the map $\{\mathtt{0},\mathtt{1}\}^*\to\mathbb{R}$ defined by $w\mapsto\mu_q(w)_{12}$ is increasing thus injective over the language of a balanced sequence. The proof uses an equivalence between balanced sequences satisfying some Markoff property and indistinguishable asymptotic pairs.

Un langage algébrique est intrinsèquement ambigu si toute grammaire qui le reconnaît est ambiguë, c'est-à-dire qu'elle génère un même mot de deux façons différentes. Décider l'intrinsèque ambiguïté d'un langage algébrique est un problème difficile, indécidable en général. Dans les années 70-80, les preuves d'intrinsèque ambiguïté reposaient essentiellement sur des raisonnements subtils et difficiles sur les arbres de dérivation des grammaires. En 1987, Flajolet a proposé une nouvelle approche pour montrer que certains langages algébriques sont intrinsèquement ambigus, en montrant que leur série génératrice n'est pas algébrique. Cette approche s'est avérée très efficace : en utilisant cette méthode, Flajolet a démontré ou redémontré dans son article l'intrinsèque ambiguïté d'une dizaine de langages, dont plusieurs étaient des conjectures de son époque. Dans cet exposé, je propose quelques extensions qui étendent le lien entre la non-ambiguïté des langages et les séries génératrices, et apportent notamment quelques pistes de réponses à deux questions posées par Flajolet à la fin de son article.

Travail mené conjointement avec Eric Finster et Matthieu Sozeau (https://arxiv.org/abs/2105.00024).

La théorie des types de Martin-Löf peut être vue comme une fondation des mathématiques. Il a été montré que certains de ses modèles validaient une interprétation homotopique des types, ce qui a motivé une nouvelle ligne de développement de celle-ci nommée théorie des types homotopiques.

Dans cette théorie, les types ne sont pas vus comme de simples ensembles car ils ont une structure d'infini-groupoïde non-triviale conférée par leurs types identité. D'où l'idée de formaliser des résultats d'algèbre supérieure en exploitant la structure supérieure des types. Néanmoins, décrire celle-ci de façon interne reste une question ouverte. C'est à dire que l'on peut énoncer des propositions concernant des infini-groupoïdes arbitraires mais que l'on ne sait pas construire une large classe d'infini-groupoïdes, en particulier ceux dont la structure supérieure n'est pas triviale ou tronquée à partir d'une certaine dimension.

Nous proposons une approche consistant à étendre la théorie des types avec un univers de monades polynomiales satisfaisant leurs lois de façon définitionnelle. Cela nous permet de présenter les types et leur structure supérieure, et ainsi d'internaliser un certain nombre de résultats dont le fait que les types sont des infini-groupoïdes.

In the context of the development of the Coq proof assistant, I have created and maintained a multi-function bot to assist developers in automating some basic and repetitive tasks. In this talk, I will present a recent pull request that was submitted to the bot repository and this will be an opportunity to present the way the bot is architectured, and how it uses a modern, typed, GitHub API and suitable OCaml libraries to implement its features, and how that makes it easy to extend.

Graph transformation allows to extend formal language theory to the generation of graph languages. This has applications in areas such as model-driven software engineering, natural language processing, and shape analysis of programs.

We start from the well-established theory of context-free grammars based on hyperedge replacement (HR) and introduces a modest extension, contextual hyperedge replacement (CHR), in order to extend their generative power. We discuss the generative power and other properties of CHR, and relate them to HR.

Then we consider parsing for CHR grammars. As for HR, parsing is NP-complete in general, so that efficient parsing algorithms can only be achieved for subclasses. We have devised two algorithms, called predictive top-down (PTD) and predictive shift-reduce (PSR), which are inspired by the well-known LL(k) and LR(k) parsing for strings, and are usually linear, at most quadratic. We illustrate the ideas of these algorithms by graph transformation rules.

Finally we demonstrate Mark Minas' graph parser generator Grappa, which implements not only PTD and PSR parsing, including the needed analysis tools, but also generalized PSR, where parallel parsing allows to cope with ambiguous grammars. Measurements of generated parsers validate our theoretical findings regarding complexity.

Zoom meeting registration link

YouTube live stream