Introduction to Lambda Calculus
Please log in to watch this conference skillscast.
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.
In this talk Maciek will aim to present the basics of lambda calculus: its syntax, reduction rules and properties, and how the calculus can be used to model programs that we write in higher-level languages. If time permits Maciek will briefly mention a couple of more advanced topics such as Curry-Howard correspondence, combinatory logic and advanced type system features.
The talk falls primarily into the ""Functional programming theory/practice"" category. It will have very few references to Scala -- mostly illustrating how certain features of Scala have their roots in lambda calculus.
YOU MAY ALSO LIKE:
Thanks to our sponsors
Introduction to Lambda Calculus
Maciek Makowski
Maciek has spent the last ten years developing software for banks. He is interested in techniques that can advance software development practice from craft to engineering.
-
SkillsCast
Please log in to watch this conference skillscast.
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.
In this talk Maciek will aim to present the basics of lambda calculus: its syntax, reduction rules and properties, and how the calculus can be used to model programs that we write in higher-level languages. If time permits Maciek will briefly mention a couple of more advanced topics such as Curry-Howard correspondence, combinatory logic and advanced type system features.
The talk falls primarily into the ""Functional programming theory/practice"" category. It will have very few references to Scala -- mostly illustrating how certain features of Scala have their roots in lambda calculus.
YOU MAY ALSO LIKE:
Thanks to our sponsors
-
About the Speaker
Introduction to Lambda Calculus
Maciek Makowski
Maciek has spent the last ten years developing software for banks. He is interested in techniques that can advance software development practice from craft to engineering.