@inproceedings{queue,
    author = {Michael, Maged M. and Scott, Michael L.}, title = {Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms},
    booktitle = {Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing},
    series = {PODC '96},
    year = {1996},
    isbn = {0-89791-800-2},
    location = {Philadelphia, Pennsylvania, USA},
    pages = {267--275},
    numpages = {9},
    url = {http://doi.acm.org/10.1145/248052.248106},
    doi = {10.1145/248052.248106},
    acmid = {248106},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {compare_and_swap, concurrent queue, lock-free, multiprogramming, non-blocking},
} 

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

@inproceedings{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},
 url = {http://doi.acm.org/10.1145/2815400.2815402},
 doi = {10.1145/2815400.2815402},
 acmid = {2815402},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@inproceedings{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},
 url = {http://doi.acm.org/10.1145/1629575.1629596},
 doi = {10.1145/1629575.1629596},
 acmid = {1629596},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {isabelle/hol, l4, microkernel, sel4},
} 


@inproceedings{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},
 url = {http://dl.acm.org/citation.cfm?id=3026877.3026879},
 acmid = {3026879},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 

@inproceedings{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},
 url = {http://doi.acm.org/10.1145/1806596.1806610},
 doi = {10.1145/1806596.1806610},
 acmid = {1806610},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {operating system, run-time system, type safety, verification},
}

@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{go, 
author={J. Meyerson}, 
journal={IEEE Software}, 
title={The Go Programming Language}, 
year={2014}, 
volume={31}, 
number={5}, 
pages={104-104}, 
keywords={Andrew Gerrand;C;Go;Google;arrays;build times;compilers;garbage collection;golang;imports;interfaces;open source;readability;scalability;slices;standard library;syntax}, 
doi={10.1109/MS.2014.127}, 
ISSN={0740-7459}, 
month={Sept},}

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

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


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

@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{kkb-sigos,
    author  = "小久保翔平 and 伊波立樹 and 河野真治",
    title   = "Monad に基づくメタ計算を基本とする Gears OS の設計",
    journal = "第133回情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
    month   = "May",
    year    = 2015
}

@article{ikkun-sigos,
    author  = "東恩納琢偉 and 伊波立樹 and 河野真治",
    title   = "Gears OS における並列処理",
    journal = "第140回 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
    month   = "May",
    year    = 2017
}

@misc{openmp,
    title = "OpenMP: Simple, portable, scalable SMP programming",
    howpublished = {\url{http://www.openmp.org,}},
    note = {Accessed: 2018/02/05(Mon)}
}

@misc{cuda,
    title = {CUDA Zone | NVIDIA Developer},
    howpublished = {\url{https://developer.nvidia.com/cuda-zone}},
    note = {Accessed: 2018/02/05(Mon)}
}

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

@mastersthesis{kkb-master,
    author = "小久保 翔平",
    title  = "Code Segment と Data Segment を持つ Gears OS の 設計",
    school = "琉球大学 大学院理工学研究科 情報工学専攻",
    year   = "2016"
}