Universes of data

Peter Morris

School of Computer Science
University of Nottingham

Tuesday, 27 October 2009, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: Dependently typed functional programming provides exciting opportunities for programming language research. The possibilities for describing data invariants, finer program control, and code safety are reasonably well established. However, many challenges remain, for instance the type proliferation problem, and the trustability of the core theory of a language. In this talk I will present an approach to internalising the treatment of data types in a dependently typed functional programming language, using the notion of Universes. I will show how this approach has implications for both problems outlined above. The ideas I will present in this talk provide the framework for the data-types in the implementation of Epigram 2, an experimental language which I will also spend some time describing.

ERDF
Tarmo Uustalu
Last update 13.11.2009