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 fonctionnelleLe 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 posteObjectifL'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éeMois 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édiairesImplé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 macrosConcevoir 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 évaluationExplorer 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ésMois 7 à 9 : Infrastructure de macrosConcevoir 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 évaluationExplorer 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étencesCompétences scientifiques et techniquesSolides 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éesFamiliarité 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.AvantagesRestauration subventionnéeTransports publics remboursés partiellementCongé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 professionnelleRémunération2695€ brut par mois basé sur votre expérience

• Programmation
• Anglais
• Langages de programmation
• Scheme