introduction

[bitonic-mengthesis.git] / thesis.bib

diff --git a/thesis.bib b/thesis.bib
index 58bfa8954c4badb9fff55f39599a0ff60e4e3596..10bedd2cdea94caaf35b9adc4dbdb0d0d5bcc66c 100644 (file)
--- a/thesis.bib
+++ b/thesis.bib
@@ -29,9 +29,9 @@
 
 @online{GHC,
   author = {{The GHC Team}},
-  title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
+  title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.3},
   url = {http://www.haskell.org/ghc/docs/latest/html/users_guide/},
-  howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
+  howpublished = {\url{http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/}},
   year = 2012
 }
 
@@ -356,7 +356,7 @@ year = {2012}
 }
 
 @UNPUBLISHED{Huet1988,
-  author = {Huet, Gerard},
+  author = {Huet, Gerard P.},
   title = {Extending The Calculus of Constructions with Type:Type},
   note = {Unpublished draft},
   year = {1988},
@@ -562,11 +562,29 @@ year = {2012}
 
 @article{huet1973undecidability,
   title={The undecidability of unification in third order logic},
-  author={Huet, Gerard P},
+  author={Huet, Gerard P.},
   journal={Information and Control},
   volume={22},
   number={3},
   pages={257--267},
   year={1973},
   publisher={Elsevier}
-}
\ No newline at end of file
+}
+
+@article{dybjer1997representing,
+  title={Representing inductively defined sets by wellorderings in Martin-L{\"o}f's type theory},
+  author={Dybjer, Peter},
+  journal={Theoretical Computer Science},
+  volume={176},
+  number={1},
+  pages={329--335},
+  year={1997},
+  publisher={Elsevier}
+}
+
+@inbook{Nordstrom1990,
+  author = {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith, Jan M.},
+  title = {Programming in Martin-L{\"o}f Type Theory: An Introduction},
+  publisher = {Oxford University Press},
+  year = {1990}
+}