Can abstract mathematical proofs be ran as programs?

The social activities of proving and programming are traditionally thought as related but distinct. Agda is a functional proof language demonstrating that they can instead be fruitfully regarded as two sides of the same coin, notwithstanding the infinities modern mathematics abounds with.

This unification allows us to give integrated developments of algorithms which are correct by construction, to appreciate mathematics from a new computational angle, and to unlock novel ways of collaborative proof engineering and proof mining.

In order to help clarify how Agda might support your research, the talk will feature a short but complete case study in formalization – implementing and verifying the correctness of insertion sort – and also discuss Agda’s current limitations.

Speaker

Ingo Blechschmidt is a guest lecturer from Augsburg (Germany). He works in applied topos theory at the intersection of algebraic geometry and constructive mathematics.

Time and Place

Wednesday 02/04/2025, any time, from home :)

Note. Ingo cannot join us in person. Instead he has recorded his talk. You are invited to watch this recording at your own pace when you see fit. You can mail Ingo and Guillermo to discuss any questions or comments may have about the topic.