Abstracts.2019.AgdaIntro

Jesper Cockx, How to formalize stuff in Agda

Languages based on dependent type theory can be used for two different purposes: as a strongly typed programming language, or as a proof assistant for formalizing mathematics. Since they are part of the same language, each of these purposes reinforces the other: we can prove properties of our programs, and we can write programs that produce proofs. In this talk, we will see this power in action by formalizing stuff in the dependently typed programming language slash proof assistant Agda. More concretely, we will (1) define the mathematical structure of partial orders, (2) implement a generic binary search trees and insertion of new elements into them, and (3) prove that this function is implemented correctly (time permitting).

Ps: no previous knowledge of Agda is required to follow the talk!

Link to the code: https://gist.github.com/jespercockx/ddb5b31d4566fe189b455fab755fc0b3