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.