@misc{golang_impl,
    title = {josharian/impl},
    howpublished = {\url{https://github.com/josharian/impl}},
}

@misc{eclipse.jdt.ls,
    title = {Eclipse JDT Language Server},
    howpublished = {\url{https://github.com/eclipse/eclipse.jdt.ls}},
}

@misc{babel,
    title = {Babel},
    howpublished = {\url{https://babeljs.io/}},
}

@misc{eclipse_pull322,
    title = {Add unimplemented methods code action},
    author = {yaohaizh},
    organization = "GitHub",
    url = {\url{https://github.com/eclipse/eclipse.jdt.ls/pull/322}},
    refdate = "2021-01-21",
}

@misc{vscode-go,
    title = {golang/vscode-go},
    author = {golang},
    organization = "GitHub",
    url = {\url{https://github.com/golang/vscode-go}},
    refdate = "2021-01-21",
}

@misc{rpi,
  title     = "{Raspberry Pi}",
  howpublished    = {https://www.raspberrypi.org}
}

@misc{xv6rpi,
author    = {Zhiyi Wang},
title     = "{xv6-rpi}",
howpublished      = "{\url{https://code.google.com/archive/p/xv6-rpi/}}",
year      = {2013}
}

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


@misc{Yang:2010:SLI:1806596.1806610,
 author = {Yang, Jean and Hawblitzel, Chris},
 title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
 booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '10},
 year = {2010},
 isbn = {978-1-4503-0019-3},
 location = {Toronto, Ontario, Canada},
 pages = {99--110},
 numpages = {12},
 doi = {10.1145/1806596.1806610},
 acmid = {1806610},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {operating system, run-time system, type safety, verification},
}

@misc{Klein:2009:SFV:1629575.1629596,
 author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June 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 OS Kernel},
 booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
 series = {SOSP '09},
 year = {2009},
 isbn = {978-1-60558-752-3},
 location = {Big Sky, Montana, USA},
 pages = {207--220},
 numpages = {14},
 doi = {10.1145/1629575.1629596},
 acmid = {1629596},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {isabelle/hol, l4, microkernel, sel4},
}

@article{Sigurbjarnarson:2016:PVF:3026877.3026879,
 author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
 title = {Push-button Verification of File Systems via Crash Refinement},
 booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
 series = {OSDI'16},
 year = {2016},
 isbn = {978-1-931971-33-1},
 location = {Savannah, GA, USA},
 pages = {1--16},
 numpages = {16},
 acmid = {3026879},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
}



@article{
  hyperKernel,
  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},
  journal = {Proceedings of the 26th Symposium on Operating Systems Principles},
year = 2017
}



@article{
    agda-ryokka,
    author = "外間政尊 and 河野真治",
    title = "GearsOS の Hoare Logic をべースにした検証手法",
    journal = "ソフトウェアサイエンス研究会",
    month = "Jan",
    year = 2019
}

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

@InProceedings{llvm,
author    = {Chris Lattner and Vikram Adve},
title     = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}",
booktitle = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)}",
address   = {Palo Alto, California},
month     = {Mar},
year      = {2004}
}

@manual{coq,
  author = "{the coq proof assistant}",
  title ="{\url{https://coq.inria.fr/}}",
}

@manual{gcc,
author = "{GNU Compiler Collection (GCC) Internals}",
title ="{\url{http://gcc.gnu.org/onlinedocs/gccint/}}",
}

@article{weko_195888_1,
   author	 = "坂本 昂弘 and 桃原 優 and 河野 真治",
   title	 = "継続を用いたx.v6 kernelの書き換え",
   year 	 = "2019",
   institution	 = "琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
   journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
   number	 = "4",
   month	 = "may"
}

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



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

@misc{xv6,
author     = "{Russ Cox, Frans Kaashoek, Robert Morris}",
title    = {xv6 a simple, Unix-like teaching operating system},
howpublished   = {\url{https://pdos.csail.mit.edu/6.828/2018/xv6/book-rev11.pdf}},
}


@article{Chen:2015:UCH:2815400.2815402,
 author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai},
 title = {Using Crash Hoare Logic for Certifying the FSCQ File System},
 booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles},
 series = {SOSP '15},
 year = {2015},
 isbn = {978-1-4503-3834-9},
 location = {Monterey, California},
 pages = {18--37},
 numpages = {20},
 doi = {10.1145/2815400.2815402},
 acmid = {2815402},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@book{lions1996lions,
  title={Lions' Commentary on UNIX 6th Edition with Source Code},
  author={Lions, J.},
  isbn={9781573980135},
  lccn={55015401},
  series={Computer classics revisited},
  url={https://books.google.co.jp/books?id=OlZ3QgAACAAJ},
  year={1996},
  publisher={Peer-to-Peer Communications}
}




@misc{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},
    doi        = {10.1016/0890-5401(91)90052-4},
    acmid      = {116984},
    publisher  = {Academic Press, Inc.},
    address    = {Duluth, MN, USA},
}