LambdaConf 2015 - Write Some Idris Brian McKenna

Idris is a dependently typed programming language. Unlike most other dependently typed systems, Idris is designed specifically for writing executable programs. This workshop will slowly walk through writing a few programs using dependent types, to motivate its uses around correctness and expressivity. This workshop will be modeled similarly to LambdaConf 2014's but with new examples to demonstrate what Idris is capable of. The only prerequisite knowledge is familiarity with algebraic data types. It is important to have the Idris REPL installed, optionally with an interactive editor configuration such as Emacs' idris-mode or Vim's idris-vim.