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.