We present Flèche, an engine for the incremental validation and edition of scientific formalized documents.

Flèche provides a formal document model, based on a notion of functional interpretation for a family of languages plus algebraic effects capturing document dynamics.

Flèche targets existing systems with non-trivial interfaces and documents in their daily use.

Some features of Flèche are: a) hybrid formal documents, where natural language is intermixed with its formal counterpart; b) modular error recovery and handling of incomplete documents; c) incremental, full-project model; d) standard document edition workflow.

We have released a Flèche implementation for the Coq Proof Assistant, `coq-lsp`, that uses the Language Server Protocol (LSP) as an editor API. Together with LSP-capable editors like Visual Studio Code, `coq-lsp` provides a new user interface for the Coq system with unique characteristics.

Je présenterai des résultats sur l'énumération exacte et asymptotique de rectangulations génériques (partitions d'un rectangle en régions rectangulaires, sans point où 4 rectangles se rencontrent, et considérées selon deux relations d'équivalences, faible ou forte). Ces objets sont en correspondance avec certains modèles de cartes planaires orientées (orientations bipolaires dans le cas faible, structures transverses dans le cas fort), qui peuvent être encodées par certains chemins dans le quart de plan en appliquant une bijection due à Kenyon, Miller, Sheffield et Wilson. Je montrerai également une extension au cas de rectangulations non génériques, donnant un continuum de modèles de cartes planaires aléatoires qui s'approchent asymptotiquement du réseau régulier.

Travaux en commun avec Erkan Narmanli et Gilles Schaeffer

We study a variant of the widely popular, fast, and often used family of community detection procedures referred to as label propagation algorithms. These mechanisms also exhibit many parallels with models of opinion exchange dynamics and consensus mechanisms in distributed computing.

Initially, given a network, each vertex starts with a random label in the interval [0,1]. Then, in each round of the algorithm, every vertex switches its label to the majority label in its neighborhood (including its own label). At the first round, ties are broken towards smaller labels, while at each of the next rounds, ties are broken uniformly at random.

We investigate the performance of this algorithm on the binomial random graph G(n,p). Via a technically delicate analysis, we show that for np>n^(5/8+epsilon), the algorithm terminates with a single label a.a.s. Moreover, we show that if np = omega(n^(2/3)), a.a.s., this label is the smallest one, whereas if n^(5/8+epsilon) < np = o(n^(2/3)), the surviving label is, a.a.s., not the smallest one.

Joint work with Lyuben Lichev (Univ. Jean Monnet), Dieter Mitsche (Univ. Jean Monnet & Pontifícia Univ. Católica de Chile), and Pawel Pralat (Toronto Metropolitan Univ.).

Let $b\geq2$ be a positive integer. Then every real number $x\in[0,1]$ admits a $b$-adic representation with digits $a_k$. We call the real $x$ simply normal to base $b$ if every digit $d\in\{0,1,\dots,b-1\}$ occurs with the same frequency in the $b$-ary representation. Furthermore we call $x$ normal to base $b$, if it is simply normal with respect to $b$, $b^2$, $b^3$, etc. Finally we call $x$ absolutely normal if it is normal with respect to all bases $b\geq2$.

In the present talk we want to generalize this notion to normality in measure preserving systems like $\beta$-expansions and continued fraction expansions. Then we show constructions of numbers that are (absolutely) normal with respect to several different expansions.

Session-typed programming languages help programmers correctly implement communicating systems. Though many techniques exist for reasoning about these languages and their processes, few treat general recursive types and few are compositional. As a consequence, they cannot be applied to many useful programs and they do not support modular reasoning. In this talk, I will present a denotational semantics for Polarized Intuitionistic Processes (PIP), a session-typed proofs-as-processes interpretation of polarized intuitionistic linear logic. PIP features general recursion, channel transmission, choices, and synchronization. This semantics generalizes Kahn’s semantics for dataflow networks to support bidirectional, session-typed communication. It supports modular reasoning and validates expected program equivalences. Moreover, it is sound relative to barbed congruence (the canonical behavioural notion of process equivalence), and it is fully abstract in the absence of negative channel transmission. As a result, our semantics provides an intuitively reasonable account of session-typed communication and a foundation for reasoning about processes in more realistic session-typed languages.

Dans de nombreux écosystèmes de langages de programmation, les développeurs dépendent de plus en plus de dépendances externes en open source, disponibles via des gestionnaires de paquets. Les paquets clés qui ne sont pas maintenus présentent un risque pour les projets qui en dépendent ainsi que pour les écosystèmes. Par conséquent, des initiatives communautaires peuvent émerger au sein des écosystèmes pour résoudre ce problème en adoptant les paquets clés ayant des problèmes de maintenance. Dans mon exposé, je présenterai les résultats de l'article coécrit avec Jean-Rémy Falleri et récemment publié dans Empirical Software Engineering intitulé “A Grounded Theory of Community Package Maintenance Organizations”. Le but de celui-ci était de construire une théorie de ces organisations (CPMO), notamment leur émergence et leur mode de fonctionnement. Pour ce faire, nous avons utilisé une méthodologie qualitative appelée Grounded Theory. Nous avons analysé des documents existants provenant de plusieurs CPMO, tels que des documentations et des discussions sur des forums publics, complétés par des entretiens avec des initiateurs de CPMO. Je parlerai également de mon application de ce modèle d'organisation à l'écosystème Coq, avec la création de l'organisation Coq-community, et de l'expérience acquise par ce biais.

End of july 2023 Jeff Shallit asked me the following question: assuming that a synchronous automaton (two tapes read simultaneously) recognizes an ordering on the free monoid, is it decidable whether or not this ordering has infinite chains? infinite antichains? and questions of the like. I suspect(ed) that this is not the case but I started to work in the special unary case (the alphabet has a unique letter). I proved that these questions are decidable (it's easy), I characterized the orders that are linear and showed that the equivalence of two linear orders is polynomial (more interesting). I posted it on arxiv on september 19. Then I thought that I should enrich my introduction … and found out that these were (very) old results.

The characterization of linear synchronous orderings on the integers is mentioned in a paper of Liu and Minnes (2009), which refers to a paper of Khoussainov and Rubin (2001) where it is implicit and is obtained as a general result on unary relations (not necessarily orderings). In my talk I will also comment on these results and propose some possible (hopefully genuinely novel!) extensions.

In this talk we describe functorial data migration from a re-writing perspective, by way of the open-source CQL tool from categoricaldata.net. We describe how co-presheaves and their lifting problems can be finitely presented, how solving word problems in categories enables computational category theory, and some techniques for performing functorial data migration using chase algorithms.

Zoom meeting registration link

YouTube live stream

We present a layered method to solve a multi-agent state problem, involving Timed Automata, SMT and Reinforcement Learning. The first layer of our method, based on Timed Automata, efficiently models the systems and gives us a high-level plan. Then, in a second step, we refine our model and solve it with SMT. We combining these steps and call it the SWA-SMT solver. A main issue is that it cannot be executed in real time. To overcome this, we use SWA-SMT solutions as the initial training dataset for our final step, which aims to obtain a neural network control policy. We use reinforcement learning to train the policy. We develop and show an example where the use of this initial dataset is crucial for the overall success of the method.