Certified Software Development with Dependent Types in Idris

Lecture 1: introduction

Lecture 2: type-driven development

Lecture 3: defining data types

Lecture 4: input/output

Lecture 5: functions over types

Lecture 6: interfaces, modules, namespaces

Lecture 7: provable equality and decidability

Lecture 8: provable comparisons and sortedness

Lecture 9: expressing relations with Elem, with construction

Lecture 10: effectful computations

Lecture 11: defining EDSLs