### EXISTENTIAL LAMBDA CALCULUS

presentation

Watch presentation

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 HØST

@einarwh

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 WINJE

@JonasWinje

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.