Doctorant Relai-Thèse - Théorie et Implémentation de l'Algèbre Universelle. H/F - INRIA

A propos d'Inria

Inria, l'institut national de recherche dans les sciences et technologies du numérique, est en appui de l'État pour les stratégies nationales de recherche et d'innovation du numérique en tant qu'Agence de programmes. Inria mène plus de 300 projets de recherche et d'innovation avec ses 3500 scientifiques, ingénieurs et personnels d'appui, en partenariat avec les universités et l'écosystème numérique (entreprises, entrepreneurs, acteurs publics). Ensemble, nous explorons des domaines clés comme l'intelligence artificielle, la cybersécurité, l'informatique quantique, le Cloud, la transformation numérique de la santé, les jumeaux numériques ou encore les technologies numériques pour la défense. Nous construisons des solutions concrètes telles que des logiciels, des startups technologiques, des partenariats avec les entreprises du tissu national et des formations de pointe. Notre objectif : l'impact scientifique, technologique et industriel au service de la souveraineté numérique de la France.

Doctorant F/H Relai-thèse /Théorie et implémentation de l'algèbre universelle.

Type de contrat : CDD

Niveau de diplôme exigé : Bac +5 ou équivalent

Fonction : Doctorant

Niveau d'expérience souhaité : Jeune diplômé

A propos du centre ou de la direction fonctionnelle

Le centre Inria de Lyon est le 9ème centre de recherche Inria. Créé en janvier 2022, il regroupe environ 410 personnes au sein de 20 équipes de recherche et des services supports à la recherche.

Ses équipes sont localisées à Villeurbanne, à Lyon Gerland,Lyon Bronainsi qu'à Saint-Etienne.

Le centre de Lyon est présent dans les domaines du logiciel, du calcul distribué et haute performance, des systèmes embarqués, du calcul quantique et de respect de la vie privée dans le monde numérique, mais aussi de la santé et de la biologie numériques.

Contexte et atouts du poste

Projet

Le relai-thèse se déroulera dans le cadre du défi Inria Liberabaci, dont les objectifs sont de rendre des outils complexes tels que Hierarchy Builder ou Trocq, ainsi que des bibliothèques de mathématiques formalisées telles que mathematical components, plus accessibles à des non spécialistes de preuve formelles (e.g. étudiant·es en licence, professeur·es de mathématiques ou informatiques ou autres collègues) par le développement d'interfaces plus adaptées, nécessitants des adaptations théoriques.

Lieu

La recherche sera menée dans le laboratoire LIP de l'ENS Lyon sous la supervision locale de Cyril Cohen, au sein de l'équipe CASH.

Les frais de déplacement sont couverts dans les limites du barème en vigueur.

Mission confiée

Mission

Les objets mathématiques sont souvent organisés selon une structure hiérarchique. Une nouvelle théorie peut souvent être présentée comme une généralisation ou, inversement, comme une spécialisation d'une autre, et ce de manière non unique. Une spécification complète de cette taxonomie reste bien sûr implicite dans les écrits mathématiques, puisque l'auteur peut compter sur l'expertise du lecteur pour reconstituer les éléments pertinents pour l'argumentation en cours. Dans le cadre des mathématiques formalisées, grâce à l'utilisation d'assistants de preuve interactifs, un tel niveau implicite n'est pas possible, et il devient nécessaire de spécifier et de récupérer ces liens. Plus précisément, les utilisateurs doivent être capables d'introduire et de relier des théories abstraites, de les étendre avec de nouvelles constructions et de prouver les théorèmes pertinents. De plus, ils doivent pouvoir instancier ces théories à l'aide de modèles concrets et spécialiser des résultats précédemment établis. Dans ce travail, nous abordons ces défis sous différents angles. Tout d'abord, dans le cadre des fondements univalents, nous présentons un développement spécifique aux structures algébriques : la bibliothèque d'algèbre universelle pour UniMath. Ensuite, nous décrivons et présentons une sémantique opérationnelle pour Hierarchy Builder, un outil de haut niveau permettant de spécifier des hiérarchies mathématiques dans Rocq et d'appliquer facilement les résultats issus de théories abstraites à leurs modèles. Enfin, nous étudions la relation entre les syntaxes avec et sans portée, tant du point de vue des « Categories with Families » que d'un point de vue de l'implémentation.

Principales activités

• Étudier les aspects théoriques des structures algébriques
• Écrire du code en Rocq, elpi et éventuellement en Caml
• Publier des articles de recherche
• Présenter les activités de recherche à des collègues et à des étudiants.

Compétences

Compétences techniques et niveau requis

• Connaître très bien au moins un assistant de preuve en théorie des types dépendents.
• Connaître la méta-programmation des assistants de preuve.

Langues

• Anglais courant.

Compétences relationnelles

• Communiquer ses idées et résultats.
• Travailller en autonomie, tout en discutant desstratégies à adopter avec les autres membres du projets.
• Écouter les retours.

Compétences additionnelles appréciées

• Expertise enRocq.
• Connaissance de Rocq-ELPI et Hierarchy Builder
• Git, Github, et autres outils de dévelopement logiciels standards

Avantages

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés : 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (90 jours par an flottants) et aménagement du temps de travail
• Prestations sociales, culturelles et sportives (Association de gestion des oeuvres sociales d'Inria)
• Accès à la formation professionnelle
• Mutuelle et prévoyance avec participation employeur

Rémunération

2300 € brut/ mois