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

INRIA; Lyon; Sur place; EUR 40 000 - 60 000; Plein temps

Résumé du poste

Un laboratoire de recherche recherche un postdoctorant pour améliorer l'ergonomie des outils de preuve formelle dans le cadre du défi Liberabaci. Le candidat sera responsable de la conception de nouveaux langages et interfaces pour des bibliothèques de contenu formalisé. Un bon niveau de connaissance en Rocq et interaction humain machine est requis. Rémunération de 2788 € brut par mois, avec des avantages tels que la restauration subventionnée et le télétravail.

Prestations

Restauration subventionnée

Transports publics remboursés

Congés : 7 semaines + 10 jours RTT

Possibilité de télétravail

Prestations sociales, culturelles et sportives

Accès à la formation professionnelle

Participation employeur mutuelle santé

Qualifications

• Connaissance approfondie d'un assistant de preuve, idéalement en théorie des types dépendants.
• Compétences en interaction humain machine souhaitées.
• Anglais courant requis.

Responsabilités

• Mettre en place les outils et méthodologies nécessaires.
• Analyser les besoins et concevoir des langages.
• Documenter les logiciels et écrire des articles de recherche.

Connaissances

Assistance de preuve

Interaction humain machine

Communication des idées

Outils

Rocq

Git

Github

Description du poste

Contexte et atouts du poste

Projet

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ésentations en workshops et conférence.

Pour une meilleure connaissance du sujet de recherche proposé

Nous proposons de prendre connaissance des articles suivants.

• Matthieu Sozeau. A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning, 2009, 2 , pp.41-62. ⟨inria-00628904⟩
• Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi. Hierarchy Builder : algebraic hierarchies made easy in Coq with Elpi. FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.34 : 1 34 : 21, ⟨10.4230 / LIPIcs.FSCD.2020.34⟩. ⟨hal-02478907v6⟩
• Davide Fissore, Enrico Tassi. A new Type-Class solver for Coq in Elpi. The Coq Workshop 2023, Jul 2023, Białystok, Poland. ⟨hal-04467855⟩
• Cyril Cohen, Enzo Crance, Assia Mahboubi. Trocq : Proof Transfer for Free, Beyond Equivalence and Univalence. ACM Transactions on Programming Languages and Systems (TOPLAS), 2025, pp.1-40. ⟨10.1145 / 3737283⟩. ⟨hal-05192017⟩

Collaboration

La personne recrutée sera principalement en contact avec Cyril Cohen, Enrico Tassi et Matthieu Sozeau, mais pourra travailler également à distance avec d'autres membres de Liberabaci ou toute personne jugée pertinente pour faciliter ses travaux de recherches.

Responsabilités

La personne recrutéesera responsable de mettre en place les outils et méthodologies nécessaires à l'accomplissement de sa mission, avec l'aide des superviseurs et en allant chercher des expertises extérieures si besoin, notamment en interaction humain machine.

Principales activités

Activités principales

• Analyser les besoins et concevoir des langages et leurs interprétations en fonction
• Mettre en place l'infrastructure
• Implémenter des extensions de Rocq
• Documenter les logiciels résultants
• Collecter les expériences des utilisateur
• ices
• Écrire des articles de recherche et communiquer ses travaux à ses pair
• es

Activités supplémentaires

• Planifier ou intégrer les interfaces dans des environnements de dévelopement.
• Déterminer un schéma de maintenance à long terme pour celles‑ci.

Compétences techniques et niveau requis

• Connaître très bien au moins un assistant de preuve, de préférence en théorie des types dépendants.
• Connaissances avancées en interaction humain machine.

Langues

• Anglais courant.

Compétences relationnelles

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

Compétences additionnelles appréciées

• Expertise en Rocq.
• 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 (sauf pour les stagiaires et apprentis)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle
• Participation employeur mutuelle santé (sous conditions)

Rémunération

2788 € brut / mois