BCAM Scientific Seminar: Proving in Constructive Mathematics by Programming in Agda

Abstract
Type theory is a flavour of constructive mathematics where every mathematical object is of a certain type. From this perspective, propositions become types, and their proofs become programs inhabiting their corresponding type.

Agda is a functional programming language that tastes like Haskell and features dependent types, data types that depend on values, e.g., the type of lists of a given length. Agda is not just a programming language, but also a proof assistant: it enables one to construct proofs interactively, and to use the machine to check for the correctness of their proofs.

This talk will serve as a brief introduction to theorem proving using the proof assistant Agda. I will introduce some common definitions and demonstrate machine assisted theorem proving at work.

Link to the session: https://us06web.zoom.us/j/85836367303?pwd=YUNlRDlBUkV2NGFqem5teGcrelJrQT09