Abstracts.2019.AgdaIntro

How to formalize stuff in Agda

by Jesper Cockx

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 starting code: https://gist.github.com/jespercockx/ddb5b31d4566fe189b455fab755fc0b3

Link to complete code (including final proofs): https://gist.github.com/jespercockx/392e98b32ad98e57016ee416c2424d4e