...

[bitonic-mengthesis.git] / thesis.bib

diff --git a/thesis.bib b/thesis.bib
index 10bedd2cdea94caaf35b9adc4dbdb0d0d5bcc66c..f58ff07f5150fdb65b3c504c16a63b4e4bd6622c 100644 (file)
--- a/thesis.bib
+++ b/thesis.bib
@@ -104,22 +104,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,
+@article{Brady2013,
 author = {Brady, Edwin},
 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
 journal = {Unpublished draft},
 number = {November},
 title = {{Implementing General Purpose Dependently Typed Programming Languages}},
 url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
-year = {2012}
+year = {2013}
 }
 @article{Chapman2010,
 address = {New York, New York, USA},
@@ -208,19 +200,24 @@ publisher = {Bibliopolis},
 title = {{Intuitionistic type theory}},
 year = {1984}
 }
-@article{McBride2004,
-author = {McBride, Conor},
-doi = {10.1017/S0956796803004829},
-file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
-journal = {Journal of Functional Programming},
-month = jan,
-number = {1},
-pages = {69--111},
-title = {{The View from The Left}},
-url = {http://strictlypositive.org/view.ps.gz},
-volume = {14},
-year = {2004}
+
+@Article{McBride2004,
+   journal = {{J}ournal of {F}unctional {P}rogramming},
+   pages = {69--111},
+   number = {1},
+   volume = {14},
+   title = {The view from the left},
+   year = {2004},
+   author = {C. McBride and J. McKinna}
+}
+
+@phdthesis{Gimenez1996,
+author={Giménez, Eduardo},
+title={Un calcul de constructions infinies et son application {\`a} la v{\'e}rification de syst{\`e}mes communicants},
+school = {Ecole Normale Sup{\'e}rieure de Lyon},
+year = 1996
 }
+
 @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},
@@ -400,7 +397,6 @@ year = {2012}
   year = {1992},
   volume = {92},
   pages = {66--79},
-  organization = {Citeseer},
   file = {:/home/bitonic/docs/papers/coquand-pattern.ps:PostScript}
 }
 
@@ -421,7 +417,6 @@ year = {2012}
   author={McBride, Conor and McKinna, James},
   booktitle={Proceedings of the ACM SIGPLAN Haskell Workshop},
   year={2004},
-  organization={Citeseer}
 }
 
 @article{Bird1999,
@@ -588,3 +583,70 @@ year = {2012}
   publisher = {Oxford University Press},
   year = {1990}
 }
+
+@incollection{Gimenez1995,
+year={1995},
+isbn={978-3-540-60579-9},
+booktitle={Types for Proofs and Programs},
+volume={996},
+series={Lecture Notes in Computer Science},
+editor={Dybjer, Peter and Nordström, Bengt and Smith, Jan},
+doi={10.1007/3-540-60579-7_3},
+title={Codifying guarded definitions with recursive schemes},
+url={http://dx.doi.org/10.1007/3-540-60579-7_3},
+publisher={Springer Berlin Heidelberg},
+author={Giménez, Eduardo},
+pages={39-59}
+}
+
+@article{Capretta2005,
+  author    = {Venanzio Capretta},
+  title     = {General recursion via coinductive types},
+  journal   = {Logical Methods in Computer Science},
+  volume    = {1},
+  number    = {2},
+  year      = {2005},
+  ee        = {http://dx.doi.org/10.2168/LMCS-1(2:1)2005},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@article{Danielsson2012,
+ author = {Danielsson, Nils Anders},
+ title = {Operational semantics using the partiality monad},
+ journal = {SIGPLAN Not.},
+ issue_date = {September 2012},
+ volume = {47},
+ number = {9},
+ month = sep,
+ year = {2012},
+ issn = {0362-1340},
+ pages = {127--138},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/2398856.2364546},
+ doi = {10.1145/2398856.2364546},
+ acmid = {2364546},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {dependent types, mixed induction and coinduction, partiality monad},
+} 
+
+
+@incollection{Paulson1990,
+       Author = {Paulson, Lawrence C.},
+       Booktitle = {Logic and Computer Science},
+       Date-Modified = {2005-04-20 12:07:55 +0100},
+       Editor = {P. Odifreddi},
+       Pages = {361-386},
+       Publisher = {Academic Press},
+       Title = {{Isabelle}: The Next 700 Theorem Provers},
+       Year = {1990}}
+
+
+@book{Russell1927,
+      author       = "Whitehead, Alfred North and Russell, Bertrand Arthur
+                      William",
+      title        = "Principia mathematica; 2nd ed.",
+      publisher    = "Cambridge Univ. Press",
+      address      = "Cambridge",
+      year         = "1927",
+}
\ No newline at end of file