Skip to main content
To KTH's start page To KTH's start page

Thomas Lamiaux: Introduction and Unification of Different Approaches to Initial Semantics

Time: Wed 2023-05-31 10.00 - 12.00

Location: Albano house 1, floor 3, Room U (Kovalevsky)

Participating: Thomas Lamiaux, ENS Paris-Saclay

Export to calendar


Initial semantics aim to categorically represent programming languages as initial models, in order to axiomatise their syntax and substitution structures. To do so automatically, it relies on initiality theorems, that assert under simple conditions, if a programming language have an initiality model.

Initial semantics has been historically separated in three different traditions: one based on Marcello Fiore's work, one based on modules over monads and one based on heterogeneous substitution systems and signatures with strength. Noticeably, the different framework are poorly related to each other, and there is no clear introduction to any traditions.

In this talk, I give an introduction to initial semantic, and present our work, with Benedikt Ahrens, to write a clear presentation clarifying and unifying those traditions.