This tutorial introduces IDRIS, a general purpose functional programming language with dependent types. The goal of the IDRIS project is to build a dependently typed language suitable for verifiable systems programming. To this end, IDRIS is a compiled language which aims to generate efficient execu