Post-Doctorant F/H Expérience utilisateur·ice pour les preuves formelles en pratique.

**Type de contrat :** CDD **Niveau de diplôme exigé :** Thèse ou équivalent **Fonction :** Post-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 Bron ainsi 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 postdoc 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 et à **distance avec Enrico Tassi** de l'équipe STAMP à Sophia-Antipolis et **Matthieu Sozeau** de l'équipe GALLINETTE à Nantes. Il y aura des réunions et des rencontres régulières avec les co-superviseurs en distanciel ou en présence, ainsi que des réunions occasionnelles avec les participants des autres lots de travail du projet Liberabaci. **Les frais de déplacement sont couverts dans les limites du barème en vigueur.** **Mission confiée** ------------------- ### **Mission** Avec l'aide des membres des projets et de leurs collaborateur·ices, la personne recrutée travaillera sur des extensions et bibliothèques Rocq afin d'améliorer leur ergonomie. Il faudra revoir l'expérience utilisateur·ice depuis la prise en main du logiciel jusqu'aux usages les plus complexes. Il pourra être utile de faire des entretiens avec des utilisateur·ices du système pour comprendre leurs besoins réels. Il sera ensuite nécéssaire de concevoir de nouveaux languages spécifiques aux besoins, afin de rendre le language de tactique et de déclaration de structures de Rocq plus flexible, plus facile à explorer, mais également plus stables. Des explorations algorithmiques en théorie des types seront probablement nécessaire. Les résultats attendus de ce travail sont des nouvelles interfaces pour construire des bibliothèques de contenu formalisé en Rocq, des articles de recherches dans des proceedings de conférences et revues, ainsi que des présent