Funktsionaalsus sõltuvate tüüpidega struktuuridest


Kood: MTAT.05.107

Punkte: 1 AP

Tunde: 16 loengutundi

Lektor: Dr. Conor McBride


Kursus toimub RAKi Meetme 1.1 IKT doktorikooli projekti raames.

Functionality from Structure with Dependent Types

Dr. Conor McBride


This short course will introduce dependently typed programming, with a particular focus on expressing high-level structure in data, programming and reasoning. Dependent types provide powerful ways to improve the precision at which programmers work, but crucially also the level of abstraction. They give us the power to make things terribly difficult for ourselves, or remarkably easy, depending on how we use them. In this course, we'll look beyond the chocolate box of sweet examples in search of the structuring principles which help us get it right more often. Whenever we see patterns emerging, we'll look at how to express them directly in our programs.

This course will have a strong hands-on component, mediated in the Agda language: see for further information and installation instructions.

Course material

Varmo Vene