Till innehåll på sidan

Axel Ljungström: Introduction to Agda

Tid: On 2022-11-16 kl 13.30 - 14.15

Plats: Albano, Cramer room

Medverkande: Axel Ljungström

Exportera till kalender

Abstract

In this talk I will introduce Agda, a proof assistant and functional programming language based based on dependent type theory. While I normally use Agda to reason about homotopy theory, my goal in this talk is to show how Agda also may be used for writing certified programs/algorithms. I will focus on constructions (which I perceive to be) of computer scientific interest, such as lists and/or graphs.