foo

[bitonic-mengthesis.git] / thesis.bib

diff --git a/thesis.bib b/thesis.bib
index 60e575bc7a5b534e9d046b7121468809cedfb2d1..468ba5ce4a7e1237beee2d8cc857c618ab1882fa 100644 (file)
--- a/thesis.bib
+++ b/thesis.bib
@@ -378,16 +378,12 @@ year = {2012}
 }
 
 @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}
+    author = {Jacobs, Bart},
+    title = {Quotients in Simple Type Theory},
+    journal = {Manuscript, Math. Inst},
+    year = {1994}
 }
 
-
 @inproceedings{Hofmann1994,
   title={The groupoid model refutes uniqueness of identity proofs},
   author={Hofmann, Martin and Streicher, Thomas},
@@ -419,3 +415,102 @@ year = {2012}
   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}
+}
+
+@inproceedings{King1995,
+  title={Structuring depth-first search algorithms in Haskell},
+  author={King, David J and Launchbury, John},
+  booktitle={Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
+  pages={344--354},
+  year={1995},
+  organization={ACM}
+}
+
+@article{milner1978theory,
+  title={A theory of type polymorphism in programming},
+  author={Milner, Robin},
+  journal={Journal of computer and system sciences},
+  volume={17},
+  number={3},
+  pages={348--375},
+  year={1978},
+  publisher={Elsevier}
+}
+
+@article{dagand2012elaborating,
+  title={Elaborating inductive definitions},
+  author={Dagand, Pierre-Evariste and McBride, Conor},
+  journal={arXiv preprint arXiv:1210.6390},
+  year={2012}
+}
+
+@inproceedings{chapman2010gentle,
+  title={The gentle art of levitation},
+  author={Chapman, James and Dagand, Pierre-{\'E}variste and McBride, Conor and Morris, Peter},
+  booktitle={ACM Sigplan Notices},
+  volume={45},
+  number={9},
+  pages={3--14},
+  year={2010},
+  organization={ACM}
+}
+
+@article{dybjer2000general,
+  title={A general formulation of simultaneous inductive-recursive definitions in type theory},
+  author={Dybjer, Peter},
+  journal={Journal of Symbolic Logic},
+  pages={525--549},
+  year={2000},
+  publisher={JSTOR}
+}
\ No newline at end of file