Till innehåll på sidan

Benedikt Ahrens: Initial semantics for lambda calculi

Tid: Ti 2019-10-01 kl 10.00 - 12.00

Plats: Kräftriket, hus 5, sal 31

Medverkande: Benedikt Ahrens, University of Birmingham

Exportera till kalender

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.