- Universes for generic programs and proofs in dependent type theory (with Marcin Benke and Patrik Jansson). Nordic Journal of Computing 10 (2003), 265-269.

- Generic programs, generic proofs, and dependent types. Cambridge Computer Laboratory, theory seminar October 2003.