Doctorant (H/F) en logique et fondements mathématiques de l'informatique

Sujet de thèse :
Ce projet s'inscrit dans l'approche ”Mathematical Informatics” introduite récemment par T. Seiller. Une partie de ce programme propose une définition formelle d'algorithme, fondée sur une notion de "structure de donnée abstraite". La personne recrutée travaillera sur ces notions dans trois directions. Premièrement, il s'agira de clarifier la relation entre cette proposition de définition formelle d'algorithme et les propositions de Y. Gurevich (abstract state machines) et Y. Moschovakis (recurseurs). Deuxièmement, on cherchera à comprendre la relation entre la notion de structure de donnée abstraite et les formules logiques, au travers de la correspondence de Curry-Howard (correspondence preuves-programmes). Troisièmement, nous chercherons à développer une théorie de l'approximation des algorithmes, afin de parler de la convergence d'une suite de programme vers un algorithme. Cette troisième partie sera complémentée par des experiences sur des programmes obtenus par apprentissage.
Contexte :
La recherche s'effectuera au Laboratoire d'Informatique de Paris Nord (LIPN, UMR7030), et plus spécifiquement dans l'équipe "Logique et Vérification". La personne recrutée prendra part aux activités régulières de l'équipe (e.g. séminaires, groupes de travail), ainsi qu'aux activités du laboratoire (e.g. journées thématiques, séminaire des non permanents).