--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/reference.bib	Sat Feb 13 22:14:15 2021 +0900
@@ -0,0 +1,112 @@
+
+
+@article{agda,
+ 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},
+ doi = {10.1145/1481861.1481862},
+ acmid = {1481862},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {dependent types, programming},
+}
+
+
+
+@article{xv6,
+   author = "坂本 昂弘 and 桃原 優 and 河野 真治",
+   title  = "継続を用いたx.v6 kernelの書き換え",
+   year  = "2019",
+   institution	 = "琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
+   journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+   number = "4",
+   month = "may"
+}
+
+@article{
+    gearsOS2,
+    author = "宮城　光希 and 桃原　優 and  河野真治",
+    title = {Code Gear と Data Gear を持つ Gears OS の設計},
+    journal = {第59回プログラミング・シンポジウム},
+    month = "Jan",
+    year = 2018
+    }
+@article{
+    tauble,
+    author = "下地篤樹 and 河野真治",
+    title = {タブロー法を用いたContinuation based C プログラムの検証},
+    journal = {日本ソフトウェア科学会第23回大会},
+    year = 2006
+    }
+@article{
+    CbC,
+    author = "河野真治",
+    title = {継続を持つCの下位言語によるシステム記述},
+    journal = {日本ソフトウェア科学会第17回大会},
+    year = 2000
+    }
+@article{
+    tauble2,
+    author = "比嘉 薫 and 河野真治",
+    title = {タブロー法の負荷分散について},
+    journal = {日本ソフトウェア科学会第18回論文集},
+    year = 2001
+    }
+@article{
+    agda-ryokka,
+    author = "外間政尊 and 河野真治",
+    title = "GearsOS の Hoare Logic をべースにした検証手法",
+    journal = "ソフトウェアサイエンス研究会",
+    month = "Jan",
+    year = 2019
+}
+
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
+}
+@article{
+    llvmcbc,
+    author = "Kaito TOKKMORI and Shinji KONO",
+    title = "Implementing Continuation based language in LLVM and Clang",
+    journal = "LOLA 2015",
+    month = "July",
+    year = 2015
+}
+
+
+@article{extensionIceframework,
+    author = "{Adrien Champion, Tomoya Chiba, Naoki Kobayashi and Ryosuke Sato}",
+    title = "{ICE-based Refinement Type Discovery for Higher-Order Functional Programs}",
+    journal ="TACAS 2018",
+    year = {2018},
+}
+
+@article{HigherOrder,
+    author = "{Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe}",
+    title = "{Higher-Order Program Verification via HFL Model Checking}",
+    journal ="ESOP 2018",
+    year = {2018},
+}
+
+
+@inproceedings{EdmundM,
+    author = "{Edmund M. Clarke, Jr}",
+    booktitle = "{Model Checking, Second Edition}",
+    year = {2018},}
+    
+@misc{graph,
+    author = "{蓮尾 一郎}",
+    pagetitle = "{モデル検査入門}",
+    year = {2009},
+    URL = {http://www.kurims.kyoto-u.ac.jp/~cs/lecture2009/lecture09ModelChecking.pdf},}