SI Seminar by Igor Moreno Santos
Talk: Towards sound notional machines: a Lambda Calculus crash course
Online
Thu, Oct 28, 2021
Igor Moreno Santos presenting Towards sound notional machines: a Lambda Calculus crash course at the USI Software Institute.
Recorded Talk
Abstract
Extensive research in Computer Science Education demonstrates that learning to program is difficult. As means to tame that difficulty, instructors often resort to the use of Notional Machines: pedagogic devices that represent some aspect of programs or programming with the goal of assisting the understanding of said aspect (e.g. drawing a memory diagram for a given program execution to reason about aliasing). But how can we know that a Notional Machine is correct? How can we know that it is accurately representing what it is aiming to represent? We first investigate Notional Machines that represent aspects of the semantics of programming languages. In that context, to be able to talk about correctness we must first define precisely what aspect of a programming language semantics we want to represent, then precisely define what a given Notional Machines is and how it relates to that language. This talk is about the first step: how can one define precisely the semantics of a programming language. We will give a taste of the lambda calculus, a formalism that is widely used for this purpose in programming language research, and how ‘all you need is lambda’.