Publication

Conférences

Connecter l'écosystème OCaml à Software Heritage via opam

Software Heritage est un projet initié par Inria ayant pour but d'archiver l'ensemble des logiciels libres disponibles sur internet. Dans cet article nous présentons Software Heritage et décrivons nos travaux en lien avec l'écosystème OCaml, opam et Software Heritage. Ces travaux comprennent notamment l'ajout à Software Heritage de modules permettant l'archivage des paquets présents sur opam, le développement d'une bibliothèque OCaml permettent de travailler avec les identifiants Software Heritage, l'ajout à opam de la possibilité de récupérer sur Software Heritage des paquets qui ne sont plus disponibles et enfin la correction du dépôt opam officiel afin de retrouver les paquets déjà manquants. Aujourd'hui, 3516 paquets opam sont déjà archivés sur Software Heritage.

Un pdf est disponible: paper-swh-opam.pdf. Le code source aussi: paper-swh-opam.

Rapports

Dddddml, une forme pour les écrire tous

Ce document est un rapport de mon stage chez OCamlPro, effectué dans le cadre de ma formation en Master 2 FIIL à l'Université Paris-Saclay. J'y présente dddddml, un langage où l'on tente d'imposer une forme canonique sur les programmes afin de détecter et d'éviter la duplication de code. J'ai été encadré par Pierre Chambart.

Un pdf est disponible: internship-report-ocp.pdf. Le code source aussi: internship-report-ocp.

Vérification par preuve formelle de propriétés fonctionnelles d'algorithmes de classification

Ce document est un rapport de mes travaux en tant qu'ingénieur d'étude sur le sujet Vérification par preuve formelle de propriétés fonctionnelles d'algorithmes de classification, effectués dans le cadre de ma formation en Magistère 2 d'Informatique à l'Université Paris-Sud. J'y présente la preuve formelle par vérification déductive de propriétés des algorithmes de Parcoursup' au moyen de Why3. J'ai été encadré par Jean-Christophe Filliâtre.

Un pdf est disponible: internship-report-parcoursup.pdf. Le code source aussi: internship-report-parcoursup.

Partage d'implémentation, implémentation du partage: une bibliothèque fonctorisée de diagrammes de décision binaires

Ce document est un rapport de mes travaux de recherche sur le sujet Partage d'implémentation, implémentation du partage: une bibliothèque fonctorisée de diagrammes de décision binaires, effectués dans le cadre de ma formation en Master 1 Informatique à l'Université Paris-Saclay, j'ai été encadré par Jean-Christophe Filliâtre.

Un pdf est disponible: ter-report.pdf. Le code source aussi: ter-report.

Le psittacisme pour permettre l'oubli motivé : implémentation et vérification du lambda lifting pour le compilateur CakeML

Ce document est un rapport de mon stage Le psittacisme pour permettre l'oubli motivé : implémentation et vérification du lambda-lifting dans le compilateur CakeML, effectué dans le cadre de ma formation en Master 1 Jacques Herbrand à l'École Normale Supérieure Paris-Saclay. Ce stage s'est déroulé sous la direction conjointe de Scott Owens et de Hugo Férée.

Un pdf est disponible: internship-report-cakeml.pdf. Le code source aussi: internship-report-cakeml.

Vérification de compilation de requêtes SQL à base de traces

Ce document est un rapport de mon stage Vérification de compilation de requêtes SQL à base de traces, effectué dans le cadre de ma formation en Magistère 1 à l'Université Paris-Sud. Ce stage s'est déroulé sous la direction conjointe de Véronique Benzaken, Évelyne Contejean et Chantal Keller.

Un pdf est disponible: internship-report-datacert.pdf. Le code source aussi: internship-report-datacert.

Posters

Deep specification and verification of SQL compilation chain

Ce document est un poster que j'ai réalisé et qui a été présenté par Raphaël Cornet à la Junior Conference on Data Science and Engineering 2017. Il porte sur le travail effectué au cours de mon stage Vérification de compilation de requêtes SQL à base de traces, ainsi que sur les stages de Raphaël Cornet et d'Eunice Martins.

Un pdf est disponible: poster-jdse-2017.pdf. Le code source aussi: poster-jdse-2017.