Marcin Benke, Peter Dybjer, Patrik Jansson. Universes for Generic Programs and Proofs in Dependent Type Theory. Nord. J. Comput., 10(4):265-289, 2003.
@article{BenkeDJ03,
title = {Universes for Generic Programs and Proofs in Dependent Type Theory},
author = {Marcin Benke and Peter Dybjer and Patrik Jansson},
year = {2003},
tags = {generic programming, type theory},
researchr = {https://researchr.org/publication/BenkeDJ03},
cites = {0},
citedby = {0},
journal = {Nord. J. Comput.},
volume = {10},
number = {4},
pages = {265-289},
}