--- a/paper/reference.bib	Thu Feb 01 16:25:53 2018 +0900
+++ b/paper/reference.bib	Sat Feb 03 15:04:47 2018 +0900
@@ -1,275 +1,101 @@
-@book{Girard:1989:PT:64805,
- author    = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
- title     = {Proofs and Types},
- year      = {1989},
- isbn      = {0-521-37181-3},
- publisher = {Cambridge University Press},
- address   = {New York, NY, USA},
-}
-
-@book{opac-b1092711,
-   title = "Introduction to higher order categorical logic",
-   author = "Lambek, Joachim (mathématicien) and Scott, P. J.",
-   series = "Cambridge studies in advanced mathematics",
-   publisher = "Cambridge University Press",
-   address = "Cambridge, New York (N. Y.), Melbourne",
-   url = "http://opac.inria.fr/record=b1092711",
-   isbn = "0-521-24665-2",
-   year = 1986
-}
-
-@book{BarrM:cattcs,
-    author    = {Barr, Michael and Wells, Charles},
-    title     = {Category Theory for Computing Science},
-    publisher = {Prentice-Hall},
-    series    = {International Series in Computer Science},
-    year      = 1990,
-    note      = {Second edition, 1995},
-    isbn      = {0-13-120486-6},
-    lccn      = {QA76.9.M35B37 1990}
+@article{Alice1,
+    author     = {赤嶺一樹, 河野真治},
+    title      = {Data segment apiを用いた分散フレームワークの設計},
+    journal    = {日本ソフトウェア科学会第28回大会},
+    month      = Sep,
+    year       = {2011},
 }
 
-@article{Moggi:1991:NCM:116981.116984,
-    author     = {Moggi, Eugenio},
-    title      = {Notions of Computation and Monads},
-    journal    = {Inf. Comput.},
-    issue_date = {July 1991},
-    volume     = {93},
-    number     = {1},
-    month      = jul,
-    year       = {1991},
-    issn       = {0890-5401},
-    pages      = {55--92},
-    numpages   = {38},
-    url        = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
-    doi        = {10.1016/0890-5401(91)90052-4},
-    acmid      = {116984},
-    publisher  = {Academic Press, Inc.},
-    address    = {Duluth, MN, USA},
-}
-
-@techreport{JonesDuponcheel93,
-  author      = {M. P. Jones and L. Duponcheel},
-  title       = {Composing monads},
-  institution = {Yale University},
-  year        = {1993},
-  month       = {December},
-  number      = {YALEU/DCS/RR-1004},
-  type        = {Research Report},
-  ftp         = {ftp://ftp.cs.nott.ac.uk/nott-fp/reports/yale/RR-1004.ps}
+@article{Alice2,
+    author     = {杉本優, 河野真治},
+    title      = {分散フレームワークAliceのDataSegmentの更新に関する改良},
+    journal    = {情報処理学会システムソフトウェアとオペレーティング・システム 研究会(OS)},
+    month      = May,
+    year       = {2013},
 }
 
-@article{110009766999,
-author="Kaito, Tokumori and Shinji, Kono",
-title="The implementation of Continuation based C Compiler on LLVM/clang 3.5",
-journal="IPSJ SIG Notes",
-ISSN="",
-publisher="Information Processing Society of Japan (IPSJ)",
-year="2014",
-month="may",
-volume="2014",
-number="10",
-pages="1-11",
-URL="http://ci.nii.ac.jp/naid/110009766999/en/",
-DOI="",
+@mastersthesis{Aquarium,
+    author = "杉本 優",
+    title  = "分散フレームワークAlice上のMeta Computationと応用",
+    school = "琉球大学 大学院理工学研究科 情報工学専攻",
+    year   = "2015"
 }
 
-@inproceedings{weko_82695_1,
-   author = "大城,信康 and 河野,真治",
-   title = "Continuation based C の GCC4.6 上の実装について",
-   booktitle = "第53回プログラミング・シンポジウム予稿集",
-   year  = "2012",
-   volume = "2012",
-   number = "",
-   pages = "69--78",
-   month = "jan"
-}
-
-@misc{agda,
-    title = {The Agda wiki},
-    howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
-    note = {Accessed: 2016/01/20(Fri)}
-}
-
-@misc{agda-documentation,
-    title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation},
-    howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}},
-    note = {Accessed: 2016/01/31(Tue)}
+@mastersthesis{TreeVNC,
+    author = "谷成 雄",
+    title  = "授業やゼミ向けの画面共有システムTreeVNCの設計と実装",
+    school = "琉球大学 大学院理工学研究科 情報工学専攻",
+    year   = "2014"
 }
 
 
-
-@misc{coq,
-    title = {Welcome! | The Coq Proof Assistant},
-    howpublished = {\url{https://coq.inria.fr/}},
-    note = {Accessed: 2016/01/20(Fri)}
-}
-
-@misc{ats2,
-    title = {ATS-PL-SYS},
-    howpublished = {\url{http://www.ats-lang.org/}},
-    note = {Accessed: 2016/01/20(Fri)}
-}
-
-@misc{spin,
-    title = {Spin - Formal Verification},
-    howpublished = {\url{http://spinroot.com/spin/whatispin.html}},
-    note = {Accessed: 2016/01/20(Fri)}
-}
-
-@misc{nusmv,
-    title = {NuSMV home page},
-    howpublished = {\url{http://nusmv.fbk.eu/}},
-    note = {Accessed: 2016/01/20(Fri)}
-}
-
-@misc{cbmc,
-    title = {The CBMC Homepage},
-    howpublished = {\url{http://www.cprover.org/cbmc/}},
-    note = {Accessed: 2016/01/20(Fri)}
+@article{AliceVNC,
+    author     = {照屋のぞみ, 河野真治},
+    title      = {分散フレームワークAliceのPC画面配信システムへの応用},
+    journal    = {第57回プログラミング・シンポジウム},
+    month      = Jan,
+    year       = {2016},
 }
 
-@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)}
+@article{OverNAT,
+    author     = {照屋のぞみ, 河野真治},
+    title      = {分散システム向けのTopology Managerの改良},
+    journal    = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
+    month      = May,
+    year       = {2016},
 }
 
-
-
-@techreport{weko_142109_1,
-   author      = "小久保,翔平 and 伊波,立樹 and 河野,真治",
-   title       = "Monadに基づくメタ計算を基本とするGears OSの設計",
-   year        = "2015",
-   institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科, 琉球大学工学部情報工学科",
-   number      = "16",
-   month       = "may"
+@article{Jungle,
+    author     = {大城信康, 杉本優, 河野真治},
+    title      = {Data Segmentの分散データベースへの応用},
+    journal    = {日本ソフトウェア科学会第30回大会論文集},
+    month      = Sep,
+    year       = {2013},
 }
 
-@mastersthesis{utah-master,
-    author = "徳森海斗",
-    title  = "LLVM Clang 上の Continuation based C コンパイラ の改良",
-    school = "琉球大学 大学院理工学研究科 情報工学専攻",
-    year   = "2016"
-}
-
-@mastersthesis{kkb-master,
+@mastersthesis{GearsOS,
     author = "小久保 翔平",
     title  = "Code Segment と Data Segment を持つ Gears OS の 設計",
     school = "琉球大学 大学院理工学研究科 情報工学専攻",
     year   = "2016"
 }
 
-@misc{atton-ipsjpro,
-    author = "比嘉 健太, 河野 真治",
-    title  = "Continuation based C を用いたプログラムの検証手法",
-}
-
-@book{Pierce:2002:TPL:509043,
-    author = {Pierce, Benjamin C.},
-    title = {Types and Programming Languages},
-    year = {2002},
-    isbn = {0262162091, 9780262162098},
-    edition = {1st},
-    publisher = {The MIT Press},
+@mastersthesis{akasya,
+    author = "比嘉 健太",
+    title  = "メタ計算を用いた Continuation based C の検証手法",
+    school = "琉球大学 大学院理工学研究科 情報工学専攻",
+    year   = "2017"
 }
 
-@book{pierce2013型システム入門プログラミング言語と型の理論,
-  title={型システム入門プログラミング言語と型の理論: },
-  author={Pierce, B.C.},
-  isbn={9784274069116},
-  url={https://books.google.co.jp/books?id=Sx8UmwEACAAJ},
-  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},
+@misc{Akka,
+    title = {},
+    howpublished = {\url{}},
+    note = {Accessed: 2018/02/3(Sat)}
 }
 
-@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},
+@misc{Hezelcast,
+    title = {},
+    howpublished = {\url{}},
+    note = {Accessed: 2018/02/3(Sat)}
+}
+
+@misc{MessagePack,
+    title = {},
+    howpublished = {\url{}},
+    note = {Accessed: 2018/02/3(Sat)}
 }
 
-@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}
+@misc{dot,
+    title = {},
+    howpublished = {\url{}},
+    note = {Accessed: 2018/02/3(Sat)}
 }
-@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
-    }
+@misc{javassist,
+    title = {},
+    howpublished = {\url{}},
+    note = {Accessed: 2018/02/3(Sat)}
+}
 
-@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",
-
-}