file = {:home/bitonic/docs/papers/simply-easy.pdf:pdf},
owner = {bitonic}
}
+
+@ARTICLE{Bruijn91,
+ author = {de Bruijn, Nicolaas Govert},
+ title = {Telescopic mappings in typed lambda calculus},
+ journal = {Information and Computation},
+ year = {1991},
+ volume = {91},
+ pages = {189--204},
+ number = {2},
+ file = {:/home/bitonic/docs/papers/telescopes.pdf:PDF},
+ publisher = {Elsevier}
+}
+
+@UNPUBLISHED{Huet1988,
+ author = {Huet, Gerard},
+ title = {Extending The Calculus of Constructions with Type:Type},
+ note = {Unpublished draft},
+ year = {1988},
+ file = {:home/bitonic/docs/papers/huet-typtyp.pdf:pdf},
+ owner = {bitonic},
+ timestamp = {2013.06.10}
+}
+
+@ARTICLE{Harper1991,
+ author = {Harper, Robert and Pollack, Robert},
+ title = {Type checking with universes},
+ journal = {Theoretical computer science},
+ year = {1991},
+ volume = {89},
+ pages = {107--136},
+ number = {1},
+ file = {:/home/bitonic/docs/papers/type-checking-universes.ps.gz:PostScript},
+ publisher = {Elsevier}
+}
+
+@ARTICLE{Jacobs1994,
+ author = {Jacobs, Bart},
+ title = {Quotients in simple type theory},
+ journal = {available from the Hypatia Electronic Library: http://hypatia. dcs.
+ qmw. ac. uk},
+ year = {1994},
+ file = {:/home/bitonic/docs/papers/jacobs-quotients.pdf:PDF},
+ publisher = {Citeseer}
+}