Certified Software Development with Dependent Types in Idris

Repo with assignments (for those who sent me github account)

Lecture 1: introduction

• slides
• Philip Wadler's paper and video on Propositions as Types
• Idris

Lecture 2: type-driven development

• code

Lecture 3: defining data types

• slides
• code

Lecture 4: input/output

• slides
• code

Lecture 5: functions over types

• slides
• code

Lecture 6: interfaces, modules, namespaces

• slides
• code

Lecture 7: provable equality and decidability

• code

Lecture 8: provable comparisons and sortedness

• code

Lecture 9: expressing relations with Elem, with construction

• code

Lecture 10: effectful computations

• slides
• code

Lecture 11: defining EDSLs

• slides
• code