url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
year = {2012}
}
+
+@ARTICLE{Loh2010,
+ author = {Andres L{\"o}h and Conor McBride and Wouter Swierstra},
+ title = {A Tutorial Implementation of a Dependently Typed Lambda Calculus},
+ journal = {Fundam. Inform.},
+ year = {2010},
+ volume = {102},
+ pages = {177-207},
+ number = {2},
+ bibsource = {DBLP, http://dblp.uni-trier.de},
+ ee = {http://dx.doi.org/10.3233/FI-2010-304},
+ 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}
+}