09:30
10:30

Les bibliothèques de code vérifié par machine sont aujourd'hui organisées autour de hiérarchies de structures algébriques. Malheureusement, le langage de la théorie des types et les fonctionnalités fournies par le système Coq rendent la construction d'une hiérarchie difficile, même pour les utilisateurs experts. La difficulté commence par les choix non orthogonaux, entre le stockage des informations sous forme de champs d'enregistrement ou de paramètres, et entre l'utilisation de classes de types et de structures canoniques pour l'inférence. A cela s'ajoutent les préoccupations relatives aux performances et à la facilité d'utilisation, par un non-expert, de la hiérarchie finale.

HB fournit au concepteur de bibliothèques un langage permettant de décrire les éléments constitutifs des structures algébriques et de les assembler en une hiérarchie. De même, il fournit à l'utilisateur final des constructions linguistiques pour créer des instances (exemples) de structures et pour enseigner à l'élaborateur de Coq comment tirer parti de ces connaissances lors de l'inférence de types. Enfin, HB permet au concepteur de la bibliothèque d'améliorer la facilité d'utilisation de sa bibliothèque en fournissant des interfaces alternatives aux interfaces primitives, une fonctionnalité qui peut également être utilisée pour s'adapter aux changements apportés à la hiérarchie sans perturber le code utilisateur.

Il s'agit d'un travail conjoint avec Kazuhiko Sakaguchi, Pierre Roux et Enrico Tassi.

Salle 76