Les circuits reconfigurables FPGA (Field-Programmable Gate Arrays) constituent une cible de choix pour la mise en œuvre d'architectures matérielles spécialisées : ils exposent du parallélisme à grain très fin et offrent un accès direct au monde physique via des broches d'entrées/sorties.

Dans cet exposé, je présenterai un modèle de programmation pour mélanger calcul et interaction sur FPGA. Ce modèle de programmation permet de composer à la fois des comportements réactifs orientés flot de données et des calculs parallèles en mémoire partagée, avec de la concurrence déterministe et des performances prédictibles. Il s'est avéré suffisamment expressif pour développer des environnements d'exécution sur mesure, comme par exemple, une implémentation matérielle de la machine virtuelle OCaml ainsi qu'une bibliothèque d'exécution simplifiée pour OCaml (incluant un gestionnaire automatique de mémoire) avec appel d'accélérateurs via la FFI.

Twenty-five years ago, Kaplan and Tarjan established a striking result: there exist “purely functional, real-time deques with catenation”. In other words, there exists a data structure that supports the following operations: “push” and “pop” which insert and extract one element at the front end, “inject” and “eject” which insert and extract one element at the rear end and “concat”, the concatenation operation. Moreover, the data structure is persistent: none of the five operations modifies or destroys its argument. Finally, each operation has worst-case time complexity O(1). This presentation will provide an overview of the first ever implementation of the data structure, done in OCaml, and its verification in Rocq.

The development of distributed quantum architectures and protocols calls for adequate specification and verification techniques, which require abstracting and focusing on the basic features of quantum concurrent systems. Through the lens of process calculi, we will show that the observational limitations of quantum theory affect our capability of discriminating quantum-capable concurrent systems, yielding a coarser equivalence relation than the probabilistic case. In a nutshell, this is because a qubit value cannot be revealed without performing a measurement that inevitably alters its state. Most of the proposed behavioural equivalences fail to adhere to these prescriptions, as they allow revealing quantum states either explicitly, or implicitly by exploiting non-determinism. We have shown that this problem affects bisimilarities, as well as testing and trace equivalences and that constraining non-determinism is required for obtaining semantics that are faithful to the physical reality.

Unreachability is a property at the heart of garbage collection: if a location is unreachable, it can be safely deallocated. However, formally reasoning about unreachability is challenging. Indeed, to prove that a location is unreachable, one has to consider the whole heap and possibly multiple concurrent stacks, making local reasoning apparently out of reach. In this talk, I will present two projects tackling the challenge of unreachability.

In the first part, I will present my PhD thesis work: an Iris-fueled Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of concurrency and garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable.

In the second part, I will present another line of work about disentanglement. Disentanglement is a property of parallel programs asserting that a location allocated by a task must remain unreachable by concurrently executing tasks. Making use of disentanglement, the MPL (MaPLe) compiler for parallel ML equips programs with a blazingly fast, task-local, garbage collector. I will present DisLog, an Iris-fueled Separation Logic for verifying disentanglement, and present ongoing work on TypeDis, a type system for automatically verifying disentanglement.

Formal theorem proving is challenging for humans as well as for machines. Thanks to recent advances in LLM capabilities, we believe natural language can serve as a universal interface for reasoning about formal proofs. In this talk, 1) we introduce Pétanque, a new lightweight environment to interact with the Coq theorem prover; 2) we present two interactive proof protocols leveraging natural language as an intermediate representation for designing proof steps; 3) we implement beam search over these interaction protocols, using natural language to rerank proof candidates; and 4) we use Pétanque to benchmark our search algorithms on different datasets. We will then discuss the limitations of our approach and possible future directions.

I will present joint work with Pierre Boutillier, Hugo Herbelin, and Meven Lennon-Bertrand. We are implementing a new algorithm, described in Pierre's PhD thesis and further developed during Meven's internship, for pattern-matching elaboration in Coq. This algorithm starts from a richer form of pattern-matching than what is currently available by default in Coq, handling deep and multiple pattern-matching with dependent types, as proposed by Thierry Coquand in the 1990s, while targeting the same elementary form of pattern-matching present in the Coq kernel.

Most of the design challenges for this algorithm come from handling the equalities that appear at each level of deconstruction of dependent inductive values. I will compare three approaches: one proposed by Healfdene Goguen, Conor McBride, and James McKinna, which relies on the equivalence axiom between homogeneous and heterogeneous equalities (equivalent to the Uniqueness of Identity Proofs); a refinement proposed by Jesper Cockx, which avoids the need for axioms; and the encoding by small inversion, which moves the proofs of deconstruction of the dependencies from the term level to the type level. While these algorithms give an encoding of dependent pattern-matching into the Coq kernel, this discussion leads us to think about what could be a better primitive form of pattern-matching.

Smart contracts are programs that run on an interpreter cobbled together from a massively distributed network of mutually untrusting computers. Unsurprisingly, the unruly nature of the underlying execution engine has a profound impact on the behavior of the interpreter and thus the semantics of smart contracts.

Caught once again by my incurable curiosity, I have set out to delineate precisely what set smart contracts aside in the realm of programming languages.

This talk reports on some early results, modeling the semantics of smart contracts in a type-theoretic and monadic framework. The objective of this work is to support formal reasoning at the protocol level (that is, starting from a specification free from programming error).

We shall strive to stay on track and in good taste: the presentation will not cover any financial aspect of smart contracts.

The OCaml pattern-matching compiler is unsound, it generates incorrect code in the obscure corner case where we match on a value with mutable fields, and those fields are mutated during pattern-matching – from when clauses, allocation callbacks, or an access race in concurrent execution.

We recall the overall compilation strategy of the OCaml compiler, and explain how to weaken its optimization information to remain correct on mutable data.