La liste de toutes les unités d'enseignements que j'ai suivies,
de la math sup au M1, avec leur descriptif détaillé et la
note que j'ai obtenue, est
disponible ici.
Septembre 2009 à août 2013 : Thèse d'informatique
Preuves Formelles par SMT
Les techniques de preuves automatiques utilisées pour
décider la Satisfiabilité Modulo
Théories (SMT) sont particulièrement performantes
et utilisées de plus en plus largement sur des
problèmes allant de la preuve de logiciels à la
sécurité informatique.
On se propose d'explorer comment mettre ces performances à la
disposition de l'utilisateur de Coq, qui est un système de
preuves généraliste.
Dans un premier temps on cherchera donc à déterminer
quels sont les algorithmes critiques pour établir la
validité des résultats retournés par les
SMT-solvers. Dans un second temps, on cherchera à les
implémenter et les valider en Coq. On espère ainsi
obtenir une tactique de preuve automatique particulèrement
puissante.
Développement : SMTCoq
Publications et exposés : voir la
page Recherche
J'ai implanté en OCaml un termination checker de
systèmes de récriture, testant le critère
du terminaison sous-terme pour le graphe de dépendance
associé au système étudié. Cela se
plaçait dans le cadre
du projet
de démonstration automatique.
Le code source est
disponible ici,
et voici un
rapport
expliquant ma démarche.
Structures informatiques et logiques pour la
modélisation linguistique
Systèmes synchrones
J'ai étudié le rapport
technique A
clocked denotational semantic for Lucid-Synchrone in Coq de
Sylvain Boulmé et Grégoire Hamon. J'ai porté leur implantation
de Lucid Synchrone en Coq de la version 6.3.1 à la version 8.1.
Les sources originales sont
disponibles ici.
Pour avoir la version portée, merci de prendre contact avec moi.
J'ai rédigé
un rapport
expliquant l'article de Sylvain Boulmé et al. ainsi que mon
travail.
Juin à août 2008 : Stage de recherche en informatique
Substitutions pour le λ-calcul simplement typé en Agda
La catégorie des termes du λ-calcul simplement
typé en Agda
Dans la première partie de mon stage, j'ai
étudié les substitutions parallèles en λ-calcul
simplement typé. J'ai prouvé qu'elles formaient une
catégorie avec produits finis en utilisant l'assistant de
preuve Agda.
L'originalité de la preuve réside dans l'approche du
λ-calcul et des substitutions:
on définit le λ-calcul directement de
manière typée, sans passer par le λ-calcul
pur;
Juin-juillet 2007 : Stage de recherche en informatique
Manipulation pseudo-haptique d'entités 2D
Durant ce stage, j'ai implémenté de manière logicielle la mesure de
la pression sur une table tactile. En couplant ce capteur de
pression à un retour visuel, j'ai mis en place un système
pseudo-haptique donnant une sensation de poids ou de frottement à
des objets virtuels 2D. Ce dispositif a ensuite fait l'objet d'une
évaluation, dans le but de connaître la sensibilité de la table,
ainsi que l'effet de poids ressenti par les utilisateurs.