more stuff

[bitonic-mengthesis.git] / docs / background.bib

diff --git a/docs/background.bib b/docs/background.bib
index 328981b055fc557901a811be677a3fc65f4b927b..c1f8a16a13a1ed7e441e12e171fc97374563ee56 100644 (file)
--- a/docs/background.bib
+++ b/docs/background.bib
@@ -1,4 +1,4 @@
-
+ 
 @inbook{Thompson1991,
   author = {Thompson, Simon},
   title = {Type Theory and Functional Programming},
@@ -13,6 +13,62 @@
   year = {2002}
 }
 
+@online{Coq,
+  author = {{The Coq Team}},
+  title = {The Coq Proof Assistant},
+  url = {\url{coq.inria.fr}},
+  howpublished = {\url{http://coq.inria.fr}},
+  year = 2013
+}
+
+@online{GHC,
+  author = {{The GHC Team}},
+  title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
+  url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
+  howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
+  year = 2012
+}
+
+@online{EpigramTut,
+  author = {Conor McBride},
+  title = {Epigram: Practical Programming with Dependent Types},
+  url = {http://strictlypositive.org/epigram-notes.ps.gz},
+  howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
+  year = 2004
+}
+
+@online{Haskell2010,
+  author = {Simon Marlow},
+  title = {Haskell 2010, Language Report},
+  url = {http://www.haskell.org/onlinereport/haskell2010/},
+  howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
+  year = 2010
+}
+
+@online{LYAH,
+  author = {Miran Lipova\v{c}a},
+  title = {Learn You a Haskell for Great Good!},
+  url = {http://learnyouahaskell.com/},
+  howpublished = {\url{http://learnyouahaskell.com/}},
+  year = 2009
+}
+
+@inbook{ProgInHask,
+  author = {Graham Hutton},
+  title = {Programming in Haskell},
+  year = 2007,
+  publisher = {Cambridge University Press}
+}
+
+
+@inbook{Constable86,
+author = {Constable, Robert L. and Stuart F. Allen and H. M. Bromley and W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith},
+title = {Implementing Mathematics with the NuPRL Proof Development System},
+year = {1986},
+publisher = {Prentice-Hall},
+address = {NJ}
+}
+
 
 @article{Altenkirch2010,
 author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
@@ -45,6 +101,14 @@ title = {{Introduction to generalized type systems}},
 url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
 year = {1991}
 }
+@article{Bove2009,
+author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
+file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
+journal = {Theorem Proving in Higher Order Logics},
+title = {{A brief overview of Agda - a functional language with dependent types}},
+url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
+year = {2009}
+}
 @article{Brady2012,
 author = {Brady, Edwin},
 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
@@ -99,7 +163,7 @@ year = {1986}
 @article{Curry1934,
 author = {Curry, Haskell B.},
 file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
-journal = {Proceedings of the National Academy of Sciences of \ldots},
+journal = {Proceedings of the National Academy of Sciences of the United States of America},
 number = {1930},
 pages = {584--590},
 title = {{Functionality in combinatory logic}},
@@ -107,6 +171,14 @@ url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
 volume = {511},
 year = {1934}
 }
+@article{Dybjer1991,
+author = {Dybjer, Peter},
+file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
+journal = {Logical Frameworks},
+title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
+url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
+year = {1991}
+}
 @article{Hurkens1995,
 author = {Hurkens, Antonius J.C.},
 file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},