13:00
14:00

Les assistants de preuves basés sur les types dépendants sont parmis les outils offrant les garanties les plus fortes sur la sécurité d'un logiciel. Cependant, pour des projets pratiques et de grande envergure, ils induisent un effort de preuve conséquent limitant leur adoption. Une situation communément rencontrée est l'utilisation de types de données efficaces, mais qui se prêtent peu au raisonnement, rendant les preuves très techniques. Une solution potentielle pour gérer cette complexité repose sur le principe d'univalence, proposé par Voevodski, qui postule que la bonne notion d'égalité entre les types est celles d'isomorphismes. Ce principe permet de transporter les algorithmes et leur preuves portant sur un type de données se prêtant au raisonnement mais inefficace pour le calcul vers un type de données efficace pour le calcul, mais moins simple pour le raisonnement. Malheureusement, le principe d'univalence est incompatible avec celui d'unicité des preuves d'identités (UIP), un autre principe permettant souvent de simplifier les raisonnements. Cela signifie qu'en pratique, travailler avec le principe d'univalence nécessite de gérer les preuves d'identités finement, ce qui est complexe. Dans cet exposé, je vais présenter mes travaux et une direction de recherche pour simplifier cette tache. Cette direction s'appuye sur un outil que je développe appelé CaTT, permettant de décrire la structure algébrique des types d'identités. Je montrerais comment le travail dans cet outil peut être partiellement automatisé, et présenterai un plug-in de Coq permettant de générer des calculs sur les termes d'identités. Cela permet de réduire l'effort de preuve à fournir pour gérer les types d'identités. Par ailleurs l'incompatibilité entre les deux principes implique qu'il n'est pas possible d'utiliser simultanément une bibliothèque de preuves reposant l'univalence et une bibliothèque reposant sur UIP. En pratiques certaines utilisations de UIP sont cependant superflues, et il est parfois possible de rendre deux telles bibliothèques compatibles. Les travaux que je présenterai sont également une piste pour comprendre plus finement quand cela est possible et quel niveau d'intervention humaine est requis pour réaliser cela.

LaBRI 178