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

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.

• 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.

  ***

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.

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 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.

• 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

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