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


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

@misc{coq,
    title = {Welcome! | The Coq Proof Assistant},
    howpublished = {\url{https://coq.inria.fr/}},
    note = {Accessed: 2018/12/17(Mon)},
}

@misc{ats2,
    title = {ATS-PL-SYS},
    howpublished = {\url{http://www.ats-lang.org/}},
    note = {Accessed: 2018/12/17(Mon)},
}

@misc{rust,
    title = {Rust programming language},
    howpublished = {\url{https://www.rust-lang.org/}},
    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)}
}