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
2 5

What can be done when formalising mathematics without dependent types? I will give you new insights into this question by exploring the capability and possible limitations of the Isabelle/HOL proof assistant. I will explain what we learnt formalising Grothendieck's schemes using only Isabelle's module system called "locales".

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