...

[bitonic-mengthesis.git] / thesis.bib

diff --git a/thesis.bib b/thesis.bib
index 9519f9ffc4a98aa63a1e57005428366d21818d7d..f46fb3dc2c1dbdde13aec10ccd5cbbe963fe0786 100644 (file)
--- a/thesis.bib
+++ b/thesis.bib
@@ -12,6 +12,13 @@
   year = {2002}
 }
 
+@inbook{Queinnec2003,
+  author    = {Christian Queinnec},
+  title     = {Lisp in Small Pieces},
+  publisher = {Cambridge University Press},
+  year      = {2003},
+}
+
 @online{Coq,
   author = {{The Coq Team}},
   title = {The Coq Proof Assistant},
@@ -66,12 +73,11 @@
   publisher = Prentice-Hall
 }
 
-
 @article{Altenkirch2010,
-author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
 file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
-journal = {Functional and Logic \ldots},
-number = {Sheard 2005},
+journal = {Functional and Logic Programming},
+pages = {40--55},
 title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
 url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
 year = {2010}
@@ -215,6 +221,14 @@ url = {http://strictlypositive.org/view.ps.gz},
 volume = {14},
 year = {2004}
 }
+@phdthesis{McBride1999,
+author = {McBride, Conor},
+file = {:home/bitonic/.local/share/data/Mendeley Ltd./Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
+school = {University of Edinburgh},
+title = {{Dependently typed functional programs and their proofs}},
+url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},
+year = {1999}
+}
 @phdthesis{Norell2007,
 author = {Norell, Ulf},
 file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
@@ -280,6 +294,16 @@ title = {{System F with type equality coercions}},
 url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
 year = {2007}
 }
+@article{Tait1967,
+author = {Tait, William W.},
+file = {:home/bitonic/docs/papers/tait-normalising.pdf:pdf},
+journal = {The Journal of Symbolic Logic},
+number = {2},
+pages = {198--212},
+title = {{Intensional Interpretations of Functionals of Finite Type}},
+volume = {32},
+year = {1967}
+}
 @article{Vytiniotis2011,
 author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
 file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
@@ -304,11 +328,61 @@ title = {{Giving Haskell a promotion}},
 url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
 year = {2012}
 }
-@phdthesis{McBride1999,
-author = {McBride, Conor},
-file = {:home/bitonic/docs/papers/conorthesis.pdf:pdf},
-school = {University of Edinburgh},
-title = {{Dependently typed functional programs and their proofs}},
-url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},
-year = {1999}
+
+@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}
 }