@techreport{ryokka-sigos,
   author	 = "外間,政尊 and 河野,真治",
   title	 = "GearsOSのAgdaによる記述と検証",
   year 	 = "2018",
   institution	 = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
   number	 = "5",
   month	 = "may"
}

@misc{agda-wiki,
    title = {The Agda wiki},
    howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
}

@book{Stump:2016:VFP:2841316,
 author = {Stump, Aaron},
 title = {Verified Functional Programming in Agda},
 year = {2016},
 isbn = {978-1-97000-127-3},
 publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool},
 address = {New York, NY, USA},
}

@mastersthesis{atton-master,
    author = "比嘉健太",
    title  = "メタ計算を用いた Continuation based C の検証手法",
    school = "琉球大学 大学院理工学研究科 情報工学専攻",
    year   = "2017"
}

@mastersthesis{parusu-master,
    author = "伊波立樹",
    title  = "Gears OS の並列処理",
    school = "琉球大学 大学院理工学研究科 情報工学専攻",
    year   = "2018"
}

@article{kaito-lola,
    author  = "Kaito, Tokumori and Shinji, Kono",
    title   = "Implementing Continuation based language in LLVM and Clang",
    journal = "LOLA 2015, Kyoto",
    month   = "July",
    year    =  2015

}
@article{hoare,
    author = {Hoare, C. A. R.},
    title = {An Axiomatic Basis for Computer Programming},
    year = {1969},
    issue_date = {October 1969},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {12},
    number = {10},
    issn = {0001-0782},
    url = {https://doi.org/10.1145/363235.363259},
    doi = {10.1145/363235.363259},
    journal = {Commun. ACM},
    month = oct,
    pages = {576–580},
    numpages = {5},
    keywords = {programming language design, theory of programming’ proofs of programs, machine-independent programming, program documentation, axiomatic method, formal language definition}
}

@inproceedings{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},
 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{agda2-hoare,
    title = {Hoare Logic in Agda2},
    howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}},
    note = {Accessed: 2020/2/9(Sun)},
}

@misc{cr-ryukyu,
    title = {Hoare Logic - 並列信頼研 mercurial repository},
    howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/}},
    note = {Accessed: 2020/2/9(Sun)}
}

@misc{cbc-gcc,
    title = {cbc-gcc - 並列信頼研 mercurial repository},
    howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}},
    note = {Accessed: 2020/2/9(Sun)}
}

@inproceedings{mitsuki-prosym,
    author = "宮城光希 and 河野真治",
    title = "CodeGear と DataGear を持つ Gears OS の設計",
    booktitle = "第59回プログラミング・シンポジウム予稿集",
    year  = "2018",
    volume = "2018",
    pages = "197--206",
    month = "jan"
}

@mastersthesis{ikkun-master,
    author = "東恩納 琢偉",
    title  = "Gears OS でモデル検査を実現する方法について",
    school = "琉球大学 大学院理工学研究科 情報工学専攻",
    year   = "2021"
}

@inproceedings{EdmundM,
    author = "{Edmund M. Clarke, Jr}",
    booktitle = "{Model Checking, Second Edition}",
    year = {2018},}

@misc{spin,
    title = {Spin - Formal Verification},
    howpublished = {\url{http://spinroot.com/}},
    note = {Accessed: 2023/2/1(Wed)},
}


@misc{agda-stdlib,
    title = {agda-stdlib},
    howpublished = {\url{https://github.com/agda/agda-stdlib
}},
    note = {Accessed: 2023/2/1(Wed)},
}

@misc{rbtree,
  title={データ構造と基本アルゴリズム},
  author={渡邉},
  year={2000},
  publisher={共立出版}
}

@misc{model,
  title={コンピュータ基礎理論ハンドブック 形式的モデルと意味論},
  author={広瀬健},
  year={1994},
  publisher={丸善出版}
}