Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

Collection Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

Organisateur(s) Thierry Coquand
Date(s) 15/06/2022 - 15/06/2022
URL associée https://indico.math.cnrs.fr/event/8052/
00:00:00 / 00:00:00
5 5

Libraries of machine checked code are, nowadays, organized around hierarchies of algebraic structures. Unfortunately the language of Type Theory and the features provided by modern proof assistants make the construction of a hierarchy hard even for expert users. The difficulty begins with the non-orthogonal choices, between storing information as record fields or parameters, and between different inference mechanisms. To this, one may add the concerns about performance and about the usability, by a non expert, of the final hierarchy. Hierarchy Builder (HB), as implemented inside the Coq proof assistant, gives library designers a language to describe the building blocks of algebraic structures and to assemble them into a hierarchy. Similarly it provides the final user tools to build instances of structures and to inform the system how to take advantage of this knowledge during type inference. Finally HB lets library designers improve the usability of their library by providing alternative interfaces to the primitive ones, a feature that is also useful to accommodate changes to the hierarchy without breaking user code. This is a joint work with Kazuhiko Sakaguchi and Enrico Tassi

Informations sur la vidéo

  • Date de captation 15/06/2022
  • Date de publication 20/06/2022
  • Institut IHES
  • Langue Anglais
  • Audience Chercheurs
  • Format MP4

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow




Inscrivez-vous

  • Mettez des vidéos en favori
  • Ajoutez des vidéos à regarder plus tard &
    conservez votre historique de consultation
  • Commentez avec la communauté
    scientifique
  • Recevez des notifications de mise à jour
    de vos sujets favoris
Donner son avis