Till innehåll på sidan

Anders Mörtberg: Computer formalization of mathematics and Univalent Foundations

Tid: On 2020-06-03 kl 14.00 - 14.45

Föreläsare: Anders Mörtberg, Stockholms universitet

Plats: Zoom, meeting ID: 637 3645 9054

Abstract

As modern mathematical theories become increasingly complex it is also becoming increasingly difficult to be sure that they are free from mistakes. One way to increase reliability is to formalize them in a proof assistant - a computer program that algorithmically verifies the correctness of proofs. In the talk I will discuss computer formalization in general and Vladimir Voevodsky's Univalent Foundations program in particular. If time permits I will also talk about recent progress on giving computational meaning to these foundations.

Innehållsansvarig:webmaster@math.kth.se
Tillhör: Institutionen för matematik
Senast ändrad: 2020-05-29