Universes For Generic Programs

Stc
Date: 2009-10-01

Time: 11:45

Room: BBL room 471

Speaker: Joeri van Eekelen

Title: Universes for Generic Programs

Abstract

Generic programming, as used in the Functional Programming community, is writing programs and functions that work on many datatypes. This is done by examining the structure of the datatype definition. In dependently typed languages, we can use 'universes' to represent the structure of the datatype definition. Generic functions are then defined on this universe. In this talk, I'll show different universes, and how universe choice influences which datatypes can be represented.