Ingénieur scientifique contractuel / "Vers un système de macros expressif pour Rocq / Preuves et vérification / Bac + 5 ou équivalent

Type de contrat : CDD

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

Fonction : Ingénieur scientifique contractuel

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

A propos du centre ou de la direction fonctionnelle
-------------------------------------------------------

Le centre Inria de l'Université de Rennes est l'un des huit centres d’Inria et compte plus d'une trentaine d’équipes de recherche. Le centre Inria est un acteur majeur et reconnu dans le domaine des sciences numériques. Il est au cœur d'un riche écosystème de R\&D et d’innovation : PME fortement innovantes, grands groupes industriels, pôles de compétitivité, acteurs de la recherche et de l’enseignement supérieur, laboratoires d'excellence, institut de recherche technologique.

Contexte et atouts du poste
-------------------------------

• Objectif

L’extensibilité syntaxique constitue un élément essentiel de l’adoption et de l’utilisabilité des langages de programmation et des assistants de preuve. Elle permet aux utilisateurs de définir des abstractions adaptées à leurs domaines d’application et de bénéficier de notations de haut niveau plus concises et expressives. Aujourd’hui, Rocq dispose d’un mécanisme de notations qui offre des possibilités limitées d’extension syntaxique et ne bénéficie pas des avancées réalisées depuis plusieurs décennies dans le domaine des systèmes de macros expressifs et hygiéniques.

L’objectif de ce projet est de concevoir et développer un prototype de nouveau frontal pour Rocq fondé sur le concept de shrubbery notation, une représentation intermédiaire récemment introduite pour permettre des systèmes de macros puissants dans des langages à syntaxe non parenthésée. Inspiré des travaux menés autour des langages Racket et Rhombus, ce projet vise à doter Rocq d’un cadre robuste pour la transformation syntaxique, la définition de motifs (patterns) et de gabarits (templates), ainsi que l’expansion de macros. Le prototype devra démontrer comment des mécanismes avancés d’abstraction syntaxique peuvent être intégrés à l’écosystème Rocq tout en préservant la lisibilité des développements, la modularité des extensions et une gestion correcte des espaces de noms et des liaisons. Une attention particulière sera portée à l’interaction entre le système de macros et les spécificités du langage Rocq, ainsi qu’à l’exploration de l’intégration d’informations de typage statiques dans le processus d’expansion.

\*\*\*

Mission confiée
-------------------

Mois 1 à 3 : Analyse des besoins et conception du langage

Étudier le système actuel de notations de Rocq et ses principaux cas d’usage.

Analyser les systèmes de macros de Racket, Rhombus et le concept de shrubbery notation.

Identifier une série de sous\-ensembles du langage Rocq permettant un développement incrémental du prototype.

Concevoir une notation shrubbery adaptée à la syntaxe de Rocq et aux langages de preuves.

Mois 4 à 6 : Développement du frontal et des représentations intermédiaires

Implémenter un lecteur transformant le texte source Rocq en représentation shrubbery.

Développer les structures de données internes permettant de représenter cette notation tout en conservant les informations de localisation et de contexte.

Mettre en place une infrastructure de tests et de validation.

Mois 7 à 9 : Infrastructure de macros

Concevoir et implémenter un système générique de motifs et de gabarits adapté à la structure shrubbery.

Développer le cœur du système de macros.

Implémenter les algorithmes d’expansion et d’enforestation ainsi que la gestion d’espaces de liaison (binding spaces) personnalisables garantissant l’hygiène des macros.

Mois 10 à 12 : Fonctionnalités avancées et évaluation

Explorer l’intégration d’informations de typage statiques dans le processus d’expansion.

Développer des études de cas reproduisant et étendant les usages actuels du système de notations de Rocq.

Évaluer l’expressivité, la robustesse et l’utilisabilité de l’approche proposée.

Principales activités
-------------------------

Mois 7 à 9 : Infrastructure de macros

Concevoir et implémenter un système générique de motifs et de gabarits adapté à la structure shrubbery.

Développer le cœur du système de macros.

Implémenter les algorithmes d’expansion et d’enforestation ainsi que la gestion d’espaces de liaison (binding spaces) personnalisables garantissant l’hygiène des macros.

Mois 10 à 12 : Fonctionnalités avancées et évaluation

Explorer l’intégration d’informations de typage statiques dans le processus d’expansion.

Développer des études de cas reproduisant et étendant les usages actuels du système de notations de Rocq.

Évaluer l’expressivité, la robustesse et l’utilisabilité de l’approche proposée.

Compétences
---------------

Compétences scientifiques et techniques

• Solides connaissances en programmation fonctionnelle et en conception de langages de programmation.


• Bonne maîtrise de la théorie des langages, en particulier des notions de syntaxe abstraite, analyse syntaxique, transformations de programmes et systèmes de macros.


• Connaissances en théorie des types et en assistants de preuve, idéalement avec une expérience de Rocq/Coq ou d’un système similaire.


• Expérience du développement d’outils de compilation, d’analyse syntaxique ou de traitement de langages (parseurs, représentations intermédiaires, transformations de syntaxe).


• Bonne maîtrise d’OCaml ou capacité démontrée à développer dans ce langage.


• Capacité à lire et comprendre la littérature scientifique en anglais.

Compétences appréciées

• Familiarité avec les systèmes de macros avancés, notamment ceux de Scheme, Racket ou Rhombus.


• Connaissances des questions d’hygiène des macros, de gestion des espaces de noms et des mécanismes de liaison.


• Expérience avec les assistants de preuve, les langages à types dépendants ou les systèmes de réécriture.


• Connaissances en conception et implémentation de compilateurs ou d’environnements de développement.


• Intérêt pour les méthodes formelles et la formalisation de langages.

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 (après 6 mois d'ancienneté) et aménagement du temps de travail


• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)


• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)


• Accès à la formation professionnelle

Rémunération
----------------

2695€ brut par mois basé sur votre expérience

Informations générales
--------------------------

• Thème/Domaine : Preuves et vérification

Ingénierie logicielle (BAP E)

• Ville : NANTES


• Centre Inria : Centre Inria de l'Université de Rennes


• Date de prise de fonction souhaitée : 2026\-09\-01


• Durée de contrat : 12 mois


• Date limite pour postuler : 2026\-07\-31

Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.

Consignes pour postuler
---------------------------

Merci de soumettre en ligne : CV, lettre de motivation

Sécurité défense :

Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011\-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.

Politique de recrutement :

Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.

Contacts
------------

• Équipe Inria : GALLINETTE


• Recruteur :

Tabareau Nicolas / nicolas.tabareau@inria.fr
L'essentiel pour réussir
----------------------------

Le ou la candidate devra avoir un goût marqué pour la conception et l’implémentation de langages de programmation, ainsi qu’une forte capacité à naviguer entre aspects théoriques et développement logiciel. Une bonne maîtrise de la programmation fonctionnelle (idéalement en OCaml), un intérêt pour les systèmes de types et les assistants de preuve, ainsi qu’une aptitude à travailler de manière autonome dans un environnement de recherche collaborative seront des atouts essentiels pour mener à bien ce projet.

A propos d'Inria
--------------------

Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes\-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’institut fait appel à de nombreux talents dans plus d’une quarantaine de métiers différents. 900 personnels d’appui à la recherche et à l’innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start\-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.

Cette annonce provient de indeed. Voir l'annonce originale ↗