Benedikt Ahrens: Initial semantics for lambda calculi
Time: Tue 2019-10-01 10.00 - 12.00
Location: Kräftriket, hus 5, sal 31
Participating: Benedikt Ahrens, University of Birmingham
The research area of Initial Semantics studies data structures from a mathematical point of view. Its main goal is the development of recursion and induction principles. Recursion principles allow for the specification of operations on the data structures. Induction principles allow for the reasoning about the properties of those operations.
In this talk, I present Initial Semantics for a class of programming languages equipped with a specification of their operational semantics. There, recursion and induction principles allow for the specification of, and reasoning about, translations between programming languages which are by construction faithful with respect to their computational behaviour.
As an example, I will discuss a translation from lambda calculus with explicit substitutions to pure lambda calculus via initiality.