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.)
SMTCoq, and its extension Sniper <https://smtcoq.github.io/sniper>, is a long term project to automatically call automatic solvers from the Coq proof assistant. Tomaz will start with basic software engineering tasks to get familiar with the architecture of the project, in particular porting to the last version of Coq. Then the main objective of the project is to validate the new goal encoder of Sniper by implementing new transformations, such as the encoding of refinement types, and defunctionalization, time permitting.
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.)
The port will make it possible for Sniper to be part of Coq's CI <https://github.com/coq/coq/blob/master/dev/ci/README-users.md> which will ease a lot future developments. The new transformations will make Sniper be able to prove more goals, and will also validate the new goal encoder that is currently under development.
Argumentaire scientifique qui décrit le projet, l'état de l'art, les travaux antérieurs et les résultats attendus (20 lignes max.)
SMTCoq and Sniper are long term projects to automatically discharge some Coq goals to external SMT solvers. The objective is to provide powerful automatic tactics to Coq which, contrary to other approaches, are predictable, meaning that users have a good idea when it will succeed, and extensible, meaning that users may add their own transformations if, for instance, they work on specific data types. This last aspect will be the main goal of the project: validating the extensibility by adding new transformations. As Tomaz will be part of the project, but discovering it, he will be able to implement new transformations from a user perspective, but also to understand what is missing or inadequate and patch it. The transformations Tomaz will work on, the encodings of refinement types (and defunctionalization depending on time), have already been implemented in other projects or other proof assistants, which means that the main work will consist in finding out how to port it to Type Theory (for which I already have ideas) and implementing it in our framework. In addition to validating the extensibility of Sniper, it will provide new transformations that will be integrated to the automatic tactics, making them more expressive. Some references: • SMTCoq: A Plug-In for Integrating SMT Solvers into Coq, CAV 2017, Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett • Compositional Pre-processing for Automated Reasoning in Dependent Type Theory, CPP 2023, Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial.
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 ?
The project requires knowledge in proof assistants based on Type Theory, in OCaml, in the git tool, and a bit of docker.
Décrivez les activités qui seront confiées à·aux ingénieur·e·s (si possible, avec un planning de tâches attendues)
The first activity will be to port Sniper to the last version of Coq and submit to Coq's CI, which is evaluated to 6 days of work. The second activity is to implement in our framework the logical encodings of refinement types, which requires: • to understand the mechanism to add new transformations • to design the encodings • to get familiar with Coq's metaprogramming language Ltac2 • to implement the encodings • to document them. We expect it to take the remaining of the project if we go for 4 months. If we go for 6 months, a third activity will be to implement in our framework the logical encodings for defunctionalization. The detailed steps are the same, except that Tomaz will already be comfortable with the project.
Commentaires
Mettre à jour