Benedikt Ahrens: Initial semantics for lambda calculi

Time: Tue 2019-10-01 10.00 - 12.00

Lecturer: Benedikt Ahrens, University of Birmingham

Location: Kräftriket, hus 5, sal 31

Abstract

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.

Page responsible:webmaster@math.kth.se
Belongs to: Department of Mathematics
Last changed: Sep 30, 2019