Kood: MTAT.05.107
Punkte: 1 AP
Tunde: 16 loengutundi
Lektor: Dr. Conor McBride
Tunniplaan:
Kursus toimub RAKi Meetme 1.1 IKT doktorikooli projekti raames.
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 http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php for further information and installation instructions.