Version 1.7 a new dawn
lecture: Programming with dependent types in Idris
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.
Building robust software is a hard task these days. As software gets more complex it gets increasingly hard to reason about it, this leads to a larger attack surface for bugs and security flaws.
Some of these bugs can be completely eliminated with the introduction of type systems that keep our values at runtime in check. Type systems are in fact the most widespread mechanism to verify correctness properties of programs, with dependent types we take this to the next level.
In this talk I will introduce techniques for programming with dependent types as well as interaction with the programming language itself. Examples will present resource tracking in the type system e.g. tracking file handles and yielding compilation errors on resource leaks, modeling specifications of protocols as types and enforcing them.
Start time: 14:00
Room: Saal 6