La personne recrutée intégrera le Laboratoire des Sciences du Numérique de Nantes (LS2N) dont l’ambition est de rassembler les forces de recherche en Cybernétique et en Informatique pour développer les sciences du numérique, ouvertes sur les autres disciplines et en conscience des défis sociétaux que cela implique.

Le ou la candidate recruté.e devra contribuer à la théorie de la démonstration ou la sémantique dénotationnelle des logiques à points fixes et/ou de la correspondance preuves-programmes entre programmation récursive et preuves circulaires pour les logiques et les systèmes de type avec induction et coinduction et/ou contribuer au développement logiciel nécessaire à l'amélioration de l'utilisabilité des types et du raisonnement coinduction dans l'assistant de preuves Coq.

• Recherche fondamental en logique, sémantique et programmation.
• Formalisation en Coq.
• Recherches bibliographiques, rédaction d'articles, présentation de travaux en séminaire et conférences.