http://media.ccc.de/browse/congress/2014/31c3_-_6162_-_en_-_saal_6_-_201412281400_-_programming_with_dependent_types_in_idris_-_raichoo.html

Idris is a relatively young research programming languages that attempts to bring dependent types to general purpose programming. In this talk I will introduce the concept of dependent types and the Curry-Howard isomorphism and how these can be applied to prove properties about software and eradicate whole classes of bugs and security issues.

raichoo