Generic programming
A paper
Universes for generic programs and proofs in dependent type theory
(with Marcin Benke and Patrik Jansson). Nordic Journal of Computing 10 (2003), 265-269.
A talk
Generic programs, generic proofs, and dependent types
. Cambridge Computer Laboratory, theory seminar October 2003.