TallCat
Webpage of the Compositional Systems and Methods group at TalTech
Functional Programming
Course Organization
- course code
- ITI0212
- term
- Spring 2021
- lectures
-
Mondays 14:15 - 15:45
in ICT-507 and on Zoom - labs
-
Tuesdays 12:00 - 13:30
in ICT-402 and on Gather - instructors
- Pawel Sobocinski, Chad Nester, Ed Morehouse
Resources
- The Idris Tutorial (written for Idris 1, but mostly still applies to Idris 2)
- The Idris Book (also available from the TalTech Library)
- Idris 2 online documentation
- Idris 1 online documentation
Announcements
- All course meetings will be remote for the foreseeable future.
-
The marking criteria for homework assignments and the term project are as follows.
- correctness: 70%
- style (clarity, concision, efficiency): 30%
- Information about the final exam is now available (see below).
Assignments
- Homework 1 is due 2021.02.22.
- Homework 2 is due 2021.03.26.
- Homework 3 is due 2021.04.16.
- Homework 4 is due 2021.05.10.
Course Project
- Here is the specification. The project is due 2021.04.26.
Final Exam
- Here is information about the final exam.
Outline
| week | date | topic | lecture videos | lecture notes | lab exerceses | |
|---|---|---|---|---|---|---|
| 01 | 2021.01.25 | Course Introduction | lecture 1 | lab 1 | ||
| 02 | 2021.02.01 | Inductive Types and Recursive Functions | lecture 2 | lab 2 | ||
| 03 | 2021.02.08 | Type Constructors | lecture 3 | lab 3 | ||
| 04 | 2021.02.15 | Higher-Order Functions | lecture 4 | lab 4 | ||
| 05 | 2021.02.22 | I/O and do Notation | lecture 5 | lab 5 | ||
| 06 | 2021.03.01 | Rewiew and Questions | lecture 6 | script file | lab 6 | |
| 07 | 2021.03.08 | Totality for Data and Codata | lecture 7 | script file | lab 7 | |
| 08 | 2021.03.15 | Programming Interfaces | lecture 8 | script file | lab 8 | |
| 09 | 2021.03.22 | Algebraic Interfaces | lecture 9 | script file | lab 9 | |
| 10 | 2021.03.29 | Programming with Dependent Types | lecture 10 | script file | lab 10 | |
| 11 | 2021.04.05 | Propositions as Types | lecture 11 | script file | lab 11 | |
| 12 | 2021.04.12 | Inductive Equality | lecture 12, addendum | script file package file | lab 12 | |
| 13 | 2021.04.19 | First-Order Logic | lecture 13 | script file | lab 13 | |
| 14 | 2021.04.26 | Decidability and Automation | lecture 14 | script file | lab 14 |