Recherche

Sujets d'intérêt : Théorie des types (homotopiques), Assistant de preuve, Théorie des catégories.

Publications

2016 : Kevin Quirin, Nicolas Tabareau. Lawvere-Tierney sheafification in Homotopy Type Theory. Journal of Formalized Reasoning, [S.l.], v. 9, n. 2, p. 131-161, dec. 2016. ISSN 1972-5787. Available at: https://jfr.unibo.it/article/view/6232.

2016 : Thèse de doctorat : Lawvere-Tierney sheafification in homotopy type theory. Version à jour disponible ici.

Talks

2016 : Exposé au séminaire Pampers des jeunes chercheurs en géométrie : Le groupe fondamental du cercle en théorie des types homotopiques. (Fichier Coq)

2015 : Exposé au workshop HoTT à Varsovie (colocated with TLCA and RDA) (diaporama annoté)

2014 : Exposé aux RDHL (rencontres doctorales Henri Lebesgue) : Théorie des types homotopiques (diaporama)

Stages

2013 : Hypothèse du continu en théorie des types, sous la direction de Nicolas Tabareau, à l'École des Mines de Nantes. (rapport, diaporama)

2011 : Logique intuitionniste, sous la direction de Vítězslav Švejdar, à l'université Charles de Prague. (rapport, diaporama)

2010 : Algèbres de Poisson, sous la direction de Pol Vanhaecke à l'université de Poitiers. (rapport,diaporama)