Mathematical Structures in Dependent Type Theory

by Assia Mahboubi

  • When: Friday, 14/05/2021, between 9am and 10am EDT (1pm - 2pm UTC)
  • Where: Zoom; Outside guests please RSVP by emailing Harley Eades
  • YouTube Stream/Recording: There will be no stream or recording of this talk, please join via Zoom.

Abstract

The past decade has seen the advent of several large-scale digital libraries of formalised mathematics, written with the help of proof assistants. Most of these libraries are framed by hierarchies of formal algebraic structures. These structures play a similar role as Bourbaki’s mathematical structures, codifying the mathematical language used throughout the library, its vocabulary and its notational apparatus. The latter hierarchies can also be seen as a formal-proof-engineering device, which organises inheritance and sharing between various interfaces.

This talk will discuss the recent techniques proposed to design these hierarchies in proof assistants based on dependent type theory, the corresponding achievements, but also their pitfalls and limitations.

School of Computer and Cyber Sciences Augusta University