abstract:
Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.
bio:
David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.
The Idris materials are at https://github.com/david-christiansen/IdrisAtGalois2015