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.