@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},
}
                 

@article{atton-ipsj,
author="比嘉 健太 and 河野 真治",
title="Verification Method of Programs Using Continuation based C",
journal="情報処理学会論文誌プログラミング（PRO）",
ISSN="1882-7802",
publisher="",
year="2017",
month="feb",
volume="10",
number="2",
pages="5-5",
URL="https://ci.nii.ac.jp/naid/170000148438/en/",
DOI="",
}

@article{moggi-monad,
    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},
}

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


@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}},
    note = {Accessed: 2018/12/17(Mon)},
}


@misc{agda-documentation,
    title = {Welcome to Agda’s documentation! — Agda latest documentation},
    howpublished = {\url{http://agda.readthedocs.io/en/latest/}},
    note = {Accessed: 2018/12/17(Mon)},
}

@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},
} 

@article{10.1145/363235.363259,
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}
}
  

@misc{agda-alpa-old,
    title = {Example - Hoare Logic},
    howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}},
    note = {Accessed: 2019/1/16(Wed)},
}

@misc{agda-alpa,
    title = {Agda1},
    howpublished = {\url{https://sourceforge.net/projects/agda/}},
    note = {Accessed: 2020/2/9(Sun)},
}

@misc{agda2-hoare,
    title = {Hoare Logic in Agda2},
    howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}},
    note = {Accessed: 2020/2/9(Sun)},
}

@misc{coq-old,
    title = {Welcome! | The Coq Proof Assistant},
    howpublished = {\url{https://coq.inria.fr/}},
    note = {Accessed: 2020/2/9(Sun)},
}

                  
@misc{coq,
    title = {Coq Source},
    howpublished = {\url{https://github.com/coq/coq}},
    note = {Accessed: 2020/2/9(Sun)},
}
                  

@misc{ats2,
    title = {ATS-PL-SYS},
    howpublished = {\url{http://www.ats-lang.org/}},
    note = {Accessed: 2020/2/9(Sun)},
}

@misc{rust,
    title = {Rust programming language},
    howpublished = {\url{https://www.rust-lang.org/}},
    note = {Accessed: 2020/2/9(Sun)},
}


@article{Klein:2010:SFV:1743546.1743574,
 author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Heiser, Gernot and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
 title = {seL4: Formal Verification of an Operating-system Kernel},
 journal = {Commun. ACM},
 issue_date = {June 2010},
 volume = {53},
 number = {6},
 month = jun,
 year = {2010},
 issn = {0001-0782},
 pages = {107--115},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/1743546.1743574},
 doi = {10.1145/1743546.1743574},
 acmid = {1743574},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@inproceedings{Nelson:2017:HPV:3132747.3132748,
 author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi},
 title = {Hyperkernel: Push-Button Verification of an OS Kernel},
 booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles},
 series = {SOSP '17},
 year = {2017},
 isbn = {978-1-4503-5085-3},
 location = {Shanghai, China},
 pages = {252--269},
 numpages = {18},
 url = {http://doi.acm.org/10.1145/3132747.3132748},
 doi = {10.1145/3132747.3132748},
 acmid = {3132748},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

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

@mastersthesis{utah-master,
    author = "徳森海斗",
    title  = "LLVM Clang 上の Continuation based C コンパイラ の改良",
    school = "琉球大学 大学院理工学研究科 情報工学専攻",
    year   = "2016"
}

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

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

@mastersthesis{mitsuki-master,
    author = "宮城光希",
    title  = "継続を基本とした言語による OS のモジュール化",
    school = "琉球大学 大学院理工学研究科 情報工学専攻",
    year   = "2019"
}

@inproceedings{weko_82695_1,
   author = "大城,信康 and 河野,真治",
   title = "Continuation based C の GCC4.6 上の実装について",
   booktitle = "第53回プログラミング・シンポジウム予稿集",
   year  = "2012",
   volume = "2012",
   number = "",
   pages = "69--78",
   month = "jan"
}

@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

}


@misc{cbc-llvm,
    title = {cbc-llvm - 並列信頼研 mercurial repository},
    howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}},
    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)}
}