Ingénieur Scientifique Contractuel - Vers un Système de Macros Expressif pour Rocq - Preuves et Vérification - Bac + 5 ou Équivalent H/F - INRIA

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'eorce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.

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 coeur 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 coeur 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 coeur 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 oeuvres sociales d'Inria)
- Accès à la formation professionnelle

Rémunération

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