Projets-App
Projets
Editer un projet
Cadre de travail
Unité de recherche rattachée au CNRS
IRIF
LIPN
LMF
Information du ou de la responsable scientifique du projet :
Prénom
Nom
E-mail
Présentation du projet scientifique
Nom du project
Résumé publiable du projet (10 lignes max.)
Autosubst2 est un plugin Coq/Rocq qui sert à aider les formalisations de langages avec des variables liées, en générant des lemmes "boilerplate" pour la représentation des variables en indices de De Bruijn. (Page web : https://www.ps.uni-saarland.de/extras/autosubst2/ ) Je propose de compléter l'implémentation de Autosubst2 pour faciliter les formalisation Rocq de langages de programmation.
Champs thématiques adressés (séparés par des virgules)
Type
proof-of-concept
prototype
maintenance/évolution logiciel existant
prématuration
Décrivez les innovations attendues à l'issue du projet (5 lignes max.)
Ajout de fonctionnalités manquantes à Autosubst 2 pour gérer les binders n-aires.
Argumentaire scientifique qui décrit le projet, l'état de l'art, les travaux antérieurs et les résultats attendus (20 lignes max.)
L'outil Autosubst2 est très utile pour les gens qui font de la sémantique des langages de programmation en Rocq, mais l'implémentation la plus récente ( https://github.com/uds-psl/autosubst-ocaml ) manque certaines fonctionnalités, en particuliers pour la gestion des binders n-aires, comme par exemple la forme "let (x, y, ...) = e in e" qui peut introduire un nombre arbitraire de variables dans le contexte. Un exemple de limitation de Autosubst2 à corriger: https://github.com/uds-psl/autosubst-ocaml/issues/8 Ma compréhension de la situation est que les bases scientifiques de l'outil sont solides, mais que certaines combinaisons de possibilités ne sont pas gérées par l'implémentation actuelle. Le travail consisterait typiquement à repérer les cas problématiques, écrire de petits exemples de sorties Coq/Rocq attendues à la main, corriger le générateur de code OCaml pour généraliser ce comportement, et écrire des tests pour valider le bon fonctionnement de cette nouvelle fonctionnalité.
Description du besoin en ingénierie
Évaluez le temps ingénieur dont vous avez besoin pour votre projet:
Frequence
2 jour/semaine
3 jour/semaine
Durée
1 mois
2 mois
3 mois
4 mois
5 mois
6 mois
Quelles sont les compétences spécifiques d'ingénierie attendues ; notamment, langages ou frameworks qui seront utilisés dans le projet, outils existants, connaissances requises ?
Coq, OCaml.
Décrivez les activités qui seront confiées à·aux ingénieur·e·s (si possible, avec un planning de tâches attendues)
Extension du plugin Autosubst2 avec des fonctionnalités manquantes -- développement OCaml d'un générateur de définitions en Coq.
Commentaires
Mettre à jour