--- a/paper/reference.bib	Mon Feb 06 15:42:45 2017 +0900
+++ b/paper/reference.bib	Mon Feb 06 16:13:14 2017 +0900
@@ -129,6 +129,18 @@
     note = {Accessed: 2016/01/20(Fri)}
 }
 
+@misc{opencl,
+    title = {OpenCL | NVIDIA Developer},
+    howpublished = {\url{https://developer.nvidia.com/opencl}},
+    note = {Accessed: 2016/02/06(Mon)}
+}
+
+@misc{cuda,
+    title = {CUDA Zone | NVIDIA Developer},
+    howpublished = {\url{https://developer.nvidia.com/cuda-zone}},
+    note = {Accessed: 2016/02/06(Mon)}
+}
+
 
 
 @techreport{weko_142109_1,
@@ -164,3 +176,88 @@
   year={2013},
   publisher={オーム社}
 }
+
+@inproceedings{Norell:2009:DTP:1481861.1481862,
+ author = {Norell, Ulf},
+ title = {Dependently Typed Programming in Agda},
+ booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
+ series = {TLDI '09},
+ year = {2009},
+ isbn = {978-1-60558-420-1},
+ location = {Savannah, GA, USA},
+ pages = {1--2},
+ numpages = {2},
+ url = {http://doi.acm.org/10.1145/1481861.1481862},
+ doi = {10.1145/1481861.1481862},
+ acmid = {1481862},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {dependent types, programming},
+}
+
+@article{Backus:1978:HFI:960118.808380,
+ author = {Backus, John},
+ title = {The History of FORTRAN I, II, and III},
+ journal = {SIGPLAN Not.},
+ issue_date = {August 1978},
+ volume = {13},
+ number = {8},
+ month = aug,
+ year = {1978},
+ issn = {0362-1340},
+ pages = {165--180},
+ numpages = {16},
+ url = {http://doi.acm.org/10.1145/960118.808380},
+ doi = {10.1145/960118.808380},
+ acmid = {808380},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@ARTICLE{Landin64,
+  AUTHOR = {Peter J. Landin},
+  TITLE = {The Mechanical Evaluation of Expressions},
+  JOURNAL = {Computer Journal},
+  VOLUME = 6,
+  NUMBER = 4,
+  MONTH = JAN,
+  YEAR = 1964,
+  PAGES = {308--320},
+  CHECKED = {5 June 1992, by JCR}
+}
+@book{GlossarWiki:Church:1941,
+   author = {Church, Alonzo},
+   title = {The Calculi of Lambda-Conversion},
+   publisher = {Princeton University Press},
+   year = {1941},
+   address = {Princeton, New Jork},
+   url = {http://books.google.de/books/about/The_Calculi_of_Lambda_conversion.html?id=KCOuGztKVgcC},
+   quality = {5},
+   note = {}
+ }
+
+@article{haskell-sigplan
+    ,author="Hudak, P. and Peyton Jones, S. and Wadler (editors), P."
+    ,title="Report on the {P}rogramming {L}anguage {H}askell,
+           {A} {N}on-strict {P}urely {F}unctional {L}anguage ({V}ersion 1.2)"
+    ,journal="ACM SIGPLAN Notices"
+    ,volume=27
+    ,number=5
+    ,month=May
+    ,year=1992
+    }
+
+@article{DEBRUIJN1972381,
+title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
+journal = "Indagationes Mathematicae (Proceedings)",
+volume = "75",
+number = "5",
+pages = "381 - 392",
+year = "1972",
+note = "",
+issn = "1385-7258",
+doi = "http://dx.doi.org/10.1016/1385-7258(72)90034-0",
+url = "http://www.sciencedirect.com/science/article/pii/1385725872900340",
+author = "N.G de Bruijn",
+
+}