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.)