La théorie des ensembles sur ordinateur
avec Pierre
Pierre est en deuxième année de thèse.
Les implémentations connues de la théorie des ensembles dans un assistant de preuves comme Coq sont confrontées à
deux écueils: antagonistes. D'un coté on veut un typage sophistiqué (en particulier avec types dépendants), pour supporter les constructions les plus abstraites des mathématiques de pointe. De l'autre coté, un tel typage génère, à terme, des difficultés plus ou moins insurmontables pour l'utilisateur, difficultés dues principalement au décalage entre l'égalité meta et l'égalité objet.
La solution explorée dans la thèse de Pierre consiste à découpler le typage en
- un typage rudimentaire, de bas niveau, décidable, et vérifié par la machine, juste assez puissant pour supporter l'isomorphisme de Curry-Howard, et
- un typage sophistiqué, de haut niveau, non
décidable, et qui serait vérifié interactivement.
Pierre et moi, on trouve cette entreprise passionnante