Bienvenue sur ma page !
D'octobre 2018 à janvier 2022, j'étais doctorant au LMF sous la direction de Chantal Keller, de Claude Marché et d'Andrei Paskevich. Le sujet de ma thèse, la Certification de la transformation de tâches de preuve,
porte sur la vérification de programmes et la sûreté de cette vérification.
Plus de détails sur la page de la soutenance.
Accédez au dépôt Why3 pour voir les derniers développements !
De septembre 2016 à septembre 2018, j'étais étudiant du Master Parisien de Recherche en Informatique de Paris Diderot (M1 et M2).
De septembre 2015 à septembre 2016, j'étais étudiant du Master 2 de Mathématiques Fondamentales de Paris Diderot.
De septembre 2011 à septembre 2015, j'étais normalien à l'ENS Cachan dans le département de mathématiques de l'antenne de Bretagne et j'ai obtenu l'agrégation de mathématiques.
En bref : mon CV et ma liste de publications.
Pour l'année scolaire 2019/2020, j'étais chargé de TD des cours suivants :
Pour l'année scolaire 2018/2019, j'étais chargé de TD des cours suivants :
ENSEIGNEMENT
Pour l'année scolaire 2020/2021, j'étais chargé de TD des cours suivants :
- Langages et Interprétation en L3 de Thibaut Balabonski
- Algorithmique par Emmanuelle Frenoux pour les étudiants de troisième année à Polytech Paris-Sud
- Programmation Fonctionnelle Avancée en L3 de Pablo Arrighi
Pour l'année scolaire 2019/2020, j'étais chargé de TD des cours suivants :
- Programmation Objet et Génie Logiciel en L2 de Thibaut Balabonski
- Données et Connaissances pour le Web en M2 de Kim Nguyen
- Introduction à la Programmation Fonctionnelle en L2 de Sylvain Conchon
- Compilation et Langages de Programmation en M1 de Thibaut Balabonski
Pour l'année scolaire 2018/2019, j'étais chargé de TD des cours suivants :
- Unix et Programmation Web en L2 de Kim Nguyen
- Programmation Fonctionnelle Avancée en L3 de Sylvain Conchon
PRÉSENTATIONS / PUBLICATIONS
Soutenance de thèse, janvier 2022.
Manuscrit de thèse, Certification de la transformation de tâches de preuve, janvier 2022.
Présentation au GT LVP, novembre 2021.
Présentation à PxTP, juillet 2021.
Publication à PxTP, A Framework for Proof-carrying Logical Transformations, juillet 2021.
Présentation au séminaire Deducteam, juillet 2020.
Soutenance du mi-parcours de thèse, juin 2020.
Rapport du mi-parcours de thèse, juin 2020.
Présentation aux JFLA, janvier 2020.
Publication aux JFLA, Des transformations logiques passent leur certificat, janvier 2020.
Présentation au GT UPSCaLe, juin 2019.
Présentation aux JFLA, février 2019.
Publication aux JFLA, SMTCoq : Automatisation expressive et extensible dans Coq, janvier 2019.
Présentation au GT SCALP, novembre 2018.
Rapport de stage du M2 MPRI, Démonstration automatique en Coq, septembre 2018.
Audition de thèse, juin 2018.
CONTACT
Envoyez-moi un mail : quentin (point) garchery (arobase) lri (point) fr
Ou un courrier : LRI, Bât 650 Ada Lovelace, Université Paris Sud, 91405 Orsay Cedex, France
Sinon, venez me voir au
Laboratoire de Recherche en Informatique. Je suis au bureau 65.