@article{
    gears,
    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
    month = "May",
    year = 2016
}

@article{
    cbc,
    author = "Kaito TOKKMORI and Shinji KONO",
    title = "Implementing Continuation based language in LLVM and Clang",
    journal = "LOLA 2015",
    month = "July",
    year = 2015
}

@Misc{mitsuki:2017,
  author = "{宮城 光希, 河野 真治}",
  title = "{CbC 言語による OS 記述}",
  journal = "{琉球大学工学部情報工学科平成 29 年度学位論文}",
  year = 2017
}

@Comment Agda-Reference

@article{170000148438,
    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="",
}


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

@misc{agda,
    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},
} 


@misc{agda-alpa,
    title = {Example - Hoare Logic},
    howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}},
    note = {Accessed: 2018/12/17(Mon)}
}

@misc{agda2-hoare,
    title = {Hoare Logic in Agda2},
    howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}},
    note = {Accessed: 2018/12/17(Mon)}
}



@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: 2018/12/17(Mon)}
}