In our second episode, we speak with Edwin Brady from the University of St. Andrews. Since 2008, Edwin has been working on Idris, a functional programming language with dependent types. This episode is very much about programming: we discuss the language Idris, its history, its implementation strategies, and plans for the future.
- Inductive Families Need Not Store Their Indices by Edwin Brady, Conor McBride and James McKinna, TYPES 2003
- Practical Implementation of a Dependently Typed Functional Programming Language by Edwin Brady. PhD thesis, 2005
- Ivor, a Proof Engine by Edwin Brady
- Simply Easy! An Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and (ahem) Wouter Swierstra
- Simpler! Easier! by Lennart Augustsson
- Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation by Edwin Brady. Journal of Functional Programming volume 23 issue 5, September 2013, pp. 552-593