Chaos Communication Congress

Programming with dependent types in Idris (#6162) (31x45)

Air date: Dec 28, 2014

Speaker: raichoo 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.