How to Do Maths Without Dependent Types | Vidéo | Carmin.tv

00:00:00 / 00:00:00

How to Do Maths Without Dependent Types

By Anthony Bordg

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

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".

Information about the video

Date of recording 6/15/22
Date of publication 6/20/22
Institution IHES
Language English
Audience Researchers
Format MP4

Domain(s)

Logic in Computer Science

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

Copyright Carmin.tv 2023

Give feedback