## Indexed containers

School of Computer Science

University of Nottingham

Wednesday, 26 November 2008, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: The notion of containers has helped develop a
theory of strictly positive datatypes, which model structures such as
lists and trees. The idea behind indexed containers is to generalise
this notion to model such advanced data-types as vectors (lists of a
given length) or well scoped lambda terms.

We have developed a theory of these so called indexed families by
extending existing results from plain containers. What is most
pleasing about this new theory is that it requires no more semantic
structure than for our theory of plain containers.

In this talk I will introduce first the notion of a container and then
generalise the constructions to indexed containers, showing a number of
possible uses of this technology.

(Joint work with Thorsten Altenkirch, Neil Ghani, Peter Hancock and
Conor McBride.)

Tarmo Uustalu

Last update 4.12.2008