TallCat
Webpage of the Compositional Systems and Methods group at TalTech
Functional Programming
Course Organization
- course code
- ITI0212
- term
- Spring 2022
- lectures
-
Wednesdays 10:00 - 11:30
in ICT-315 and on Zoom - labs
-
Fridays 10:00 - 11:30
in ICT-122 and on Gather - instructors
- Matt Earnshaw, Philipp Joram, Ed Morehouse
- 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
- Due to instructor illness, lecture will be online only on 2022-03-09.
- Information about the final exam is now available (see below).
Assignments
- homework 1 is due 2022-03-02.
- homework 2 is due 2022-03-23.
- homework 3 is due 2022-04-15.
- homework 4 is due 2022-05-05.
- homework 5 is due 2022-05-25.
Course Project
- Here is the specification. The project is due 2022-05-16.
Final Exam
- Here is information about the final exam.
Outline
| week | date | topic | lecture videos | lecture notes | lab exerceses |
|---|---|---|---|---|---|
| 01 | 2022-01-26 | course introduction | lecture video | script file | lab sheet |
| 02 | 2022-02-02 | inductive types and recursive functions | lecture video | script file | lab sheet |
| 03 | 2022-02-09 | parameterized types and generic functions | lecture video | script file | lab sheet |
| 04 | 2022-02-16 | function literals and higher-order functions | lecture video | script file | lab sheet |
| 05 | 2022-02-23 | -- no lecture -- | |||
| 06 | 2022-03-02 | indexed types and dependent functions | lecture video | script file | lab sheet |
| 07 | 2022-03-09 | monadic I/O | lecture video | script file | lab sheet |
| 08 | 2022-03-16 | programming interfaces | lecture video | script file | lab sheet |
| 09 | 2022-03-23 | record types | lecture video | script file | lab sheet |
| 10 | 2022-03-30 | totality for data and codata | lecture video | script file | lab sheet |
| 11 | 2022-04-06 | computation in types | lecture video | script file | lab sheet |
| 12 | 2022-04-13 | algebraic interfaces | lecture video | script file | lab sheet |
| 13 | 2022-04-20 | propositions as types | lecture video | script file | lab sheet |
| 14 | 2022-04-27 | inductive equality | lecture video | script file | lab sheet |
| 15 | 2022-05-04 | first-order logic | lecture video | script file | lab sheet |
| 16 | 2022-05-11 | decidability and automation | lecture video | script file | lab sheet |