Generic Programming within Dependently Typed Programming.

Conor McBride

(Durham)

This is joint work with Thorsten Altenkirch

We show how higher kinded generic programming can be represented faithfully within a dependently typed programming system. The development has been implemented using the OLEG system.

The present work can be seen as evidence for our thesis that extensions of type systems can be done by programming within a dependently typed language, using data as codes for types.

More details can be found under http://www.dur.ac.uk/c.t.mcbride/generic/.
Tuesday 29th October 2002, 14:00
Robert Recorde Room
Department of Computer Science