TallCat
Webpage of the Compositional Systems and Methods group at TalTech
Functional Programming
Course Organization
- course code
- ITI0212
- term
- Spring 2023
- lectures
-
Mondays 10:00 - 11:30
in ICT-315 and on Zoom - labs
-
Fridays 08:30 - 09:30
in ICO-317 and on Gather - instructors
- Ed Morehouse, Diana Kessler
- teaching assistants
- Michele De Pascalis, Andrea Laretto
- syllabus
- here
- discord
- Join
Resources
- Some notes on installing Idris
- The Idris Website
- 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 2 standard library
Announcements
- Announcements will be posted here.
Assignments
- Homework assignments for the course will be posted here.
Course Project
- Information about the course project will be posted here in March.
Final Exam
- Information about the final exam will be posted here in April.
Outline
| week | date | topic | lecture videos | lecture notes | lab exerceses |
|---|---|---|---|---|---|
| 01 | 2023-01-30 | course introduction | |||
| 02 | 2023-02-06 | inductive types and recursive functions | |||
| 03 | 2023-02-13 | parameterized types and generic functions | |||
| 04 | 2023-02-20 | function literals and higher-order functions | |||
| 05 | 2023-02-23 | ??? | |||
| 06 | 2023-03-06 | monadic I/O | |||
| 07 | 2023-03-13 | programming interfaces | |||
| 08 | 2023-03-20 | indexed types and dependent functions | |||
| 09 | 2023-03-27 | record types | |||
| 10 | 2023-04-03 | totality for data and codata | |||
| 11 | 2023-04-10 | computation in types | |||
| 12 | 2023-04-17 | algebraic interfaces | |||
| 13 | 2023-04-24 | propositions as types | |||
| 14 | 2023-05-01 | inductive equality | |||
| 15 | 2023-05-08 | first-order logic | |||
| 16 | 2023-05-15 | decidability and automation |