JFLA 2022

Many computer systems are reactive: they execute in continuous interaction with their environment. From the perspective of functional programming, reactive systems can be modeled and programmed as stream functions. Several lines of research have exploited this point of view. Works based on Nakano’s guarded recursion use type-theoretical modalities to guarantee productivity. Works based on synchronous programming use more specialized methods but guarantee incremental processing of stream fragments. In this paper, we contribute to a recent synthesis between the two approaches by describing how a language with a family of type-theoretical modalities can be given an incremental semantics in the synchronous style. We prove that this semantics coincides with a more usual big-step semantics.

ProbZelus est un langage synchrone probabiliste qui permet de décrire des modèles probabilistes réactifs en interaction avec un environnement observable. Des méthodes d’inférences réactives permettent d’apprendre en ligne les distributions associées aux paramètres non-observés du modèle à partir d’observations statistiques. Ce problème n’a, en général, pas de solution analytique simple. Pour obtenir des estimations précises, une méthode classique consiste à analyser les résultats obtenus par de nombreuses exécutions indépendantes du modèle. Ces méthodes sont coûteuses, mais ont l’avantage de pouvoir être massivement parallélisées. Nous proposons d’utiliser JAX pour paralléliser les méthodes d’inférence réactive de ProbZelus. JAX est une bibliothèque récente qui permet de paralléliser automatiquement du code Python qui peut ensuite être exécuté de manière efficace et transparente sur CPU, GPU, ou TPU. Dans cet article, nous décrivons un nouveau moteur d’inférence réactive parallèle implémenté en JAX et le nouveau backend JAX associé pour ProbZelus. Nous montrons sur des exemples existants que notre nouvelle implémentation surpasse l’implémentation séquentielle originale pour un nombre de particules élevé.

Hydras & Co. is a collaborative library of discrete mathematics for the Coq proof assistant, developed as part of the Coq-community organization on GitHub. The Coq code is accompanied by an electronic book, generated with the help of the Alectryon literate proving tool. We present the evolution of the mathematical contents of the library since former presentations at JFLA meetings. Then, we describe how the structure of the project is determined by two requirements which must be continuously satisfied. First, the Coq code needs to be compatible with its ever-evolving dependencies (the Coq proof assistant and several Coq packages both from inside and outside Coq-community) and reverse dependencies (Coq-community projects that depend on it). Second, the book needs to be consistent with the Coq code, which undergoes frequent changes to improve structure and include new material. We believe Hydras & Co. demonstrates that books on formalized mathematics are not limited to providing exposition of theories and reasoning techniques—they can also provide inspiration and entertainment that transcends educational goals.

La vérification d’assertions à l’exécution est une technique consistant à vérifier la validité d’annotations formelles au cours de l’exécution d’un programme. Bien qu’ancienne, cette technique reste encore peu étudiée d’un point de vue théorique. Cet article contribue à pallier ce manque en formalisant un vérificateur d’assertions à l’exécution pour des propriétés arithmétiques entières. La principale difficulté réside dans la modélisation d’un générateur de code pour les propriétés visées qui génère du code à la fois correct et efficace. Ainsi, le code généré repose sur des entiers machines lorsque le générateur peut prouver qu’il est correct de le faire et sur une bibliothèque spécialisée dans l’arithmétique exacte, correcte mais moins efficace, dans les autres cas. Il utilise pour cela un système de types dédié. En outre, la logique considérée pour les propriétés inclue des constructions d’ordre supérieur. L’article présente également une implémentation de ce générateur de code au sein d’E-ACSL, le greffon de Frama-C dédié à la vérification d’assertions à l’exécution, ainsi qu’une première évaluation expérimentale démontrant empiriquement l’efficacité du code généré.

Cet article présente un système de vérification et d’inférence statique des tailles de tableaux dans un langage fonctionnel strict statiquement typé. Plutôt que de s’en remettre à des types dépendants, nous proposons un système de types proche de celui de ML. Le polymorphisme sert à définir des fonctions génériques en type et en taille. L’inférence permet une écriture allégée des opérations classiques de traitement du signal — application point-à-point, accumulation, projection, transposée, convolution — et de leur composition; c’est un atout clef de la solution proposée. Pour obtenir un bon compromis entre expressivité du langage des tailles et décidabilité de la vérification et de l’inférence, nous proposons une solution en deux temps : (i) un langage de types où les tailles sont des polynômes multi-variés et (ii) l’insertion de points de coercition explicites entre tailles dans le programme source. Lorsque le programme est bien typé, il s’exécute sans erreur de taille en dehors de ces points de coercitions. Deux usages de la proposition faite dans cet article peuvent être envisagés : (i) la génération de code défensif aux points de coercition ou, (ii) pour les applications critiques ou intensives, la vérification statique des coercitions en les limitant à des expressions évaluables à la compilation ou par des moyens d’analyse formelle comme l’interprétation abstraite. L’article définit le langage d’entrée, sa sémantique dynamique, son système de types et montre sa correction. Il est accompagné par une implémentation en OCaml, dont le code source est accessible publiquement.

Futures and promises are respectively a read-only and a write-once pointer to a placeholder in memory. They are used to transfer information between threads in the context of asynchronous concurrent programming. Futures and promises simplify the implementation of synchronisation mechanisms between threads. Nonetheless they can be error prone as data races may arise when references are shared and transferred. We aim at providing a formal tool to detect those errors. Hence, in this paper we propose a proof of concept by implementing the future/promise mechanism in Viper: a verification infrastructure, that provides a way to reason about resource ownership in programs.

K est un framework sémantique permettant de décrire formellement des sémantiques de langages de programmation. C’est aussi un environnement qui offre différents outils pour aider à la programmation avec les langages spécifiés dans le formalisme. Il est par exemple possible d’exécuter des programmes et de vérifier certaines propriétés sur ceux-ci, à l’aide de l’outil KProver. K repose sur une logique du 1er ordre munie d’une application entre formules et d’opérateurs de point fixe, d’égalité, de typage ainsi que d’un opérateur similaire à l’opérateur “next” des logiques temporelles. Ce dernier opérateur permet d’encoder la sémantique des programmes par la réécriture. Dedukti est un framework logique permettant l’interopérabilité des preuves entre différents outils de preuve formelle. Il possède des plugins d’import et d’export pour des systèmes de preuve aussi divers que Coq, PVS ou encore Isabelle/HOL. Il repose sur le LambdaPi-calcul modulo théorie, une extension de la théorie des types par l’ajout de règles de réécriture dans la relation de conversion. La flexibilité de ce logical framework permet d’encoder de nombreuses théories comme la logique du 1er ordre ou la théorie des types simples. Dans cet article, nous présentons un outil de traduction de K vers Dedukti, appelé Kamelo. Cet outil a pour objectif, à plus long terme, de permettre la vérification des preuves faites au sein de K et la réutilisation de sémantiques formelles de langages de programmation ainsi que des propriétés sur leurs programmes au sein de nombreux systèmes de preuve, via Dedukti.

Nous proposons une implémentation d’une nouvelle fonctionnalité pour OCaml, le déboîtement de constructeurs. Elle permet d’éliminer certains constructeurs de la représentation dynamique des valeurs quand cela ne crée pas d’ambiguité entre différentes valeurs au même type. Nous décrivons:

• un cas d’usage sur les grands entiers où la fonctionnalité améliore les performances de code OCaml idiomatique, éliminant le besoin d’écrire du code non-sûr,

• l’analyse statique nécessaire pour accepter ou rejeter le déboîtement d’un constructeur,

• et l’impact sur la compilation du filtrage de motif. Pour notre analyse statique, nous devons normaliser certaines expressions de type, avec une relation de normalisation qui ne termine pas nécessairement en présence de types mutuellement récursifs. Nous décrivons une analyse de terminaison qui garantit la normalisation sans rejeter les déclarations de types qui nous intéressent.

L’arithmétique flottante est connue pour être un sujet difficile. Ses propriétés contre-intuitives rendent l’écriture d’algorithmes manipulant les nombres flottants propice à de nombreuses erreurs. Des outils automatiques pour la vérification de programmes flottants existent mais ces outils mobilisant eux-même du calcul flottant, on peut se poser la question de leur propre fiabilité. Pour adresser ce problème, nous proposons de vérifier formellement l’implémentation de raisonnements sur les nombres flottants dans un solveurs CP. En particulier, nous discutons d’une méthodologie pour mener les preuves en utilisant l’assistant de preuve Coq. Nous discutons également de l’intégration des raisonnements prouvés à un développement logiciel complet en OCaml.

Les circuits reprogrammables de types FPGA constituent un matériel de choix pour la réalisation d’accélérateurs de calculs. L’implémentation O2B de la machine virtuelle OCaml permet d’appeler des circuits externes réalisés sur FPGA depuis un langage de haut niveau (OCaml) compilé en byte code. La conception de circuits s’appuie sur des langages de description de matériel (HDL) souvent fort éloignés des langages algorithmiques. C’est pourquoi l’on présente Macle, un langage applicatif dédié à la programmation de calculs séquentiels et parallèles synthétisables en circuits. On décrit la chaîne de compilation de Macle vers un HDL et son intégration à O2B.