Introduction to Lambda Calculus

Software is pervasive in the modern world and has influence over many aspects of our lives. In some cases, such as avionics or medical equipment control, human life depends on the correctness of software. Yet, high profile cases of bugs do not inspire confidence in the state of software engineering.

The “software crisis” is a phenomenon recognised by practitioners of the field. Several ways of addressing the reliability issue have been proposed: from reliance on programmer’s discipline, through tools that perform post-hoc validation of programs to ensure they do not contain suspicious coding patterns, to languages that restrict valid programs to ones whose properties can be formally proven. The latter approach relies on a body of theoretical knowledge that can appear intimidating. It turns out, however, that much of the required insight is built on systematic extensions of a very simple formal system – the lambda calculus.

While understanding of the basics of lambda calculus will not immediately make us experts in formal methods, it is a gateway to the world of software engineering tools whose roots are in logic, mathematics and formal reasoning. Lambda calculus makes the task of learning advanced programming trechniques manageable by providing a simple framework within which programming constructs can be understood.

I will be presenting an introduction to lambda calculus in November, at London Scala User Group, and in December, at Scala eXchange. If you are interested in this talk but can’t make any of those dates then I expect the videos to be available shortly after.