Accueil > Manifestations > Thèses et HDR > HDR > Nicolas Tabareau

Nicolas Tabareau

Résumé

L’appréhension de la complexité logique en mathématique offre une longue tradition de mise en place de modèles pour des logiques complexes obtenus par extension de modèles pour des logiques plus simples, comme c’est le cas pour la construction de faisceaux. En informatique, cette démarche a un pendant dual qui consiste à donner
du sens à des langages complexes via une phase de compilation vers des langages plus simples.

Dans cette exposé, je montrerai en quoi l’approche par compilation fait aussi sens en logique, via l’isomorphisme de Curry-Howard, et est en fait plus précise que l’approche par extension de modèle car elle prend en compte le calcul. Pour illustrer mon propos, je montrerai des exemples de transformation de programmes en théorie des types, avec une application à l’assistant de preuve Coq, et dans une moindre mesure en programmation distribuée.

Composition du jury :

  • Hugo Herbelin, Inria Paris, Rapporteur
  • Daniel Hirschkoff, Ens Lyon, Rapporteur
  • Alan Schmitt, Inria Rennes Bretagne Atlantique, Rapporteur
  • Claude Jard, Université de Nantes, Examinateur
  • Thierry Coquand, Göteborg University, Examinateur

Dernière modification : jeudi 17 novembre 2016