I want to learn Idris, both as a language to develop with, and to understand its underlying theory and to hack on its compiler.
Edwin Brady’s PhD thesis Practical Implementation of a Dependently Typed Functional Programming Language (2005) describes the implementation of a dependently typed core language, TT, that compiles to a G-machine. It likely forms the basis of Idris, which first appeared shortly thereafter in 2007. The thesis complements work that was being done concurrently at Durham on Epigram, a dependently typed functional programming language, by Conor McBride and James McKinna.
Edwin gave four lectures for the Oregon Programming Languages Summer School in 2017 on “Dependent Types in the Idris Programming Languages”. Videos are also linked on his site.
He wrote Type-Driven Development with Idris (2017), which teaches development using Idris. When reading it for Idris 2, it requires several small changes to update it.
He’s also written a few blog posts on Idris. In a post explaining why Idris 2 is faster than Idris 1, he mentions, that it takes insights from Andras Kovacs’ work on smalltt.
Idris documentation has more resources.
I should consider applying to be a PhD student under him.