Till innehåll på sidan
Till KTH:s startsida Till KTH:s startsida

Stefania Damato: Initial Algebra Semantics for QIITs using Containers

Tid: On 2024-06-26 kl 10.00 - 12.00

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

Medverkande: Stefania Damato

Exportera till kalender

Abstract

It is well known that ordinary inductive types and inductive families can be described semantically as initial algebras of container functors and indexed container functors respectively. In this talk, I will present ongoing work on a similar initial algebra semantics for the more general class of quotient inductive-inductive types (QIITs). A semantic framework for QIITs has already been developed in [1]. Our proposed approach is to introduce restrictions to this framework, including restricting the functors in this framework to generalised containers, to carve out those QIIT specifications that are guaranteed to have an initial algebra.

[1] : Altenkirch, Thorsten & Capriotti, Paolo & Dijkstra, Gabe & Kraus, Nicolai & Forsberg, Fredrik. (2018). Quotient Inductive-Inductive Types. 10.1007/978-3-319-89366-2_16.