# Seminario di Logica Permanente

## Venerdì 21 Giugno 2013, ore 14:30-17:30 - Aula 2AB45 - L. Malatesta, U. Grandi, E. Bottazzi

ARGOMENTI: Seminari

Seminario di Logica Permanente
Venerdì 21 Giugno 2013, ore 14:30-17:30
Aula 2AB45

Talks:
Lorenzo Malatesta (Strathclyde)
"Initial algebra semantics of small inductive-recursive definitions"
Category theory provides for a foundational framework for data types via initial algebra semantics. At the simplest level, polynomials and containers give a theory of data types as free standing entities. At a second level of complexity, dependent polynomials and indexed containers handle more sophisticated data types in which the data has an associated index which can be used to store important computational information.The crucial and salient feature of dependent polynomials and indexed containers is that the indices are defined in advance of the data. At the most sophisticated level, induction-recursion allows us to define data with indexes where the indices are defined simultaneously with the data.In this seminar I will present the relationship between the theory of inductive recursive definitions and the theory of dependent polynomials and indexed containers. The central result is that the expressiveness of small inductive recursive definitions is exactly the same as that of dependent polynomials and indexed containers. We introduce the category of small inductive-recursive definitions and prove the equivalence of this category with the category of dependent polynomials.
This is a joint work with Peter Hancock, Conor McBride, Neil Ghani and Thorsten Altenkirch.