lul

[bitonic-mengthesis.git] / thesis.bib

diff --git a/thesis.bib b/thesis.bib
index a45ff86c58712ea2fdc309dcfe560555fcc68c58..5ca5dc0b0b1bcee24c7ecb760727edead3d3194e 100644 (file)
--- a/thesis.bib
+++ b/thesis.bib
@@ -328,3 +328,146 @@ title = {{Giving Haskell a promotion}},
 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}
+}
+
+
+@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