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}
+}
+
+@inproceedings{McBride2004b,
+ title={I am not a number: I am a free variable},
+ author={McBride, Conor and McKinna, James},
+ booktitle={Proceedings of the ACM SIGPLAN Haskell Workshop},
+ year={2004},
+ organization={Citeseer}
+}
+
+@article{Bird1999,
+ title={De Bruijn notation as a nested datatype},
+ author={Richard S. Bird and Ross Paterson},
+ journal={J. Functional Programming},
+ volume={9},
+ number={1},
+ pages={77--91},
+ year={1999},
+ publisher={Cambridge Univ Press}
+}
+
+@inproceedings{de1972lambda,
+ title={Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
+ author={de Bruijn, Nicolaas Govert},
+ booktitle={Indagationes Mathematicae (Proceedings)},
+ volume={75},
+ number={5},
+ pages={381--392},
+ year={1972},
+ organization={Elsevier}
+}
+
+@article{henglein1993type,
+ title={Type inference with polymorphic recursion},
+ author={Henglein, Fritz},
+ journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
+ volume={15},
+ number={2},
+ pages={253--289},
+ year={1993},
+ publisher={ACM}
+}
+
+@inproceedings{weirich2011binders,
+ title={Binders unbound},
+ author={Weirich, Stephanie and Yorgey, Brent A and Sheard, Tim},
+ booktitle={ACM SIGPLAN Notices},
+ volume={46},
+ number={9},
+ pages={333--345},
+ year={2011},
+ organization={ACM}
+}
\ No newline at end of file