Qui suis-je ?
Je suis postdoctorant a l'Université de Pennsylvanie. Je m'intéresse a des problèmes de sécurité pour le projet CRASH/SAFE, sous la direction de Benjamin Pierce.
Avant cela, j'étais étudiant en thèse au sein du projet Gallium, à l'INRIA Paris-Rocquencourt, sous la direction de Didier Rémy. Je m'intéressais alors aux systèmes de modules, l'abstraction de types, la générativité, et aux sortes singleton.
Nouveautés
- Octobre 2012: Mise en ligne de la vérification mécanisée en Coq de l'article Robust declassification, par Steve Zdancewicz et Andrew C. Myers.
- Juillet 2012: soumission d'un article intitulé A Theory on Information-Flow Labels.
- Octobre 2011: Papier accepté au Workshop PLOS'11 (Cascais, Portugal) Preliminary Design of the SAFE Platform. La présentation que j'ai donnée est disponible.
- Décembre 2010: Mise en ligne du vérificateur de types Fzip: un vérificateur de types pour un langage explicitement typé, qui comprend du polymorphisme, des types existentiels ouverts, des sortes singleton et du sous-typage.
- Décembre 2010: Soutenance de ma thèse, intitulée "Programmer avec des modules de première classe dans un langage noyau pourvu de sous-typage, sortes singletons et types existentiels ouverts". Le manuscrit et les transparents sont disponibles en ligne.
- Septembre 2010: Les transparents de mon exposé à WMM'10 sont en ligne! Le résumé que j'ai soumis est aussi disponible pour plus de détails.
- Avril 2010: Une formalisation en Coq (version 8.2pl1) de la sûreté du système CoreFzip, avec l'aide des outils Ott et LNgen. [Sources | Html]
- Août 2009: Quelques résultats sur la combinaison de relation (confluence, bonne fondaison), formalisés en Coq (version 8.2-1). Les principaux lemmes sont ceux de Hindley-Rosen, d'Akama et la condition de Di Cosmo-Piperno-Geser. [Sources | Html]
