In earlier talks at flatMap(Oslo), we have seen that the untyped lambda calculus is tremendously powerful - using enterprise patterns such as the AbstractionRecursionFactoryFactory (aka y-combinator) and Dependency Injection (to defeat the laws of mathematics) we arrived at full Turing Completeness. However, this power comes at a cost: it is easy to make mistakes!
It is entirely possible to write programs in untyped lambda calculus that engage in infinite recursion or other nonsensical activities. For this reason, modern languages like Idris and Système F sacrifice some expressive power in order to enjoy greater safety.
In this talk, Jonas will address Einar's growing concerns about the correctness of large-scale lambda calculus programs by introducing a formalism for specifying the types of lambda calculus expressions.
Einar W. Høst is an ivory tower expat and computer programmer working for Computas, programming computers. His goal is to write code that respects and amuses the djinns of the computer but not necessarily anyone else. He holds a PhD in Computer Science from the University of Oslo.
Jonas is a developer at Computas. His favourite animal is the goat, and his favourite animal is the otter. He's got an MSc in Computer Science from the University of Oslo, his favourite animal is the quokka, and he likes programming languages. His favourite animal is the capybara.
