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}
+}
+
+
+@inproceedings{Hofmann1994,
+ title={The groupoid model refutes uniqueness of identity proofs},
+ author={Hofmann, Martin and Streicher, Thomas},
+ booktitle={Logic in Computer Science, 1994. LICS'94. Proceedings., Symposium on},
+ pages={208--212},
+ year={1994},
+ organization={IEEE}
+}
+
+@INPROCEEDINGS{Coquand1992,
+ author = {Coquand, Thierry},
+ title = {Pattern matching with dependent types},
+ booktitle = {Informal proceedings of Logical Frameworks},
+ year = {1992},
+ volume = {92},
+ pages = {66--79},
+ organization = {Citeseer},
+ file = {:/home/bitonic/docs/papers/coquand-pattern.ps:PostScript}
+}
+
+@INPROCEEDINGS{Abel2007,
+ author = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
+ title = {Normalization by evaluation for Martin-Lof type theory with typed
+ equality judgements},
+ booktitle = {Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium
+ on},
+ year = {2007},
+ pages = {3--12},
+ organization = {IEEE},
+ file = {:/home/bitonic/docs/papers/nbe.pdf:PDF}
+}