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



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

@article{
    gearsOS2,
    author = "宮城　光希 and 桃原　優 and  河野真治",
    title = {Code Gear と Data Gear を持つ Gears OS の設計},
    journal = {第59回プログラミング・シンポジウム},
    month = "Jan",
    year = 2018
    }
@article{
    tauble,
    author = "下地篤樹 and 河野真治",
    title = {タブロー法を用いたContinuation based C プログラムの検証},
    journal = {日本ソフトウェア科学会第23回大会},
    year = 2006
    }
@article{
    CbC,
    author = "河野真治",
    title = {継続を持つCの下位言語によるシステム記述},
    journal = {日本ソフトウェア科学会第17回大会},
    year = 2000
    }
@article{
    tauble2,
    author = "比嘉 薫 and 河野真治",
    title = {タブロー法の負荷分散について},
    journal = {日本ソフトウェア科学会第18回論文集},
    year = 2001
    }
@article{
    agda-ryokka,
    author = "外間政尊 and 河野真治",
    title = "GearsOS の Hoare Logic をべースにした検証手法",
    journal = "ソフトウェアサイエンス研究会",
    month = "Jan",
    year = 2019
}

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


@article{extensionIceframework,
    author = "{Adrien Champion, Tomoya Chiba, Naoki Kobayashi and Ryosuke Sato}",
    title = "{ICE-based Refinement Type Discovery for Higher-Order Functional Programs}",
    journal ="TACAS 2018",
    year = {2018},
}

@article{HigherOrder,
    author = "{Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe}",
    title = "{Higher-Order Program Verification via HFL Model Checking}",
    journal ="ESOP 2018",
    year = {2018},
}


@inproceedings{EdmundM,
    author = "{Edmund M. Clarke, Jr}",
    booktitle = "{Model Checking, Second Edition}",
    year = {2018},}
    
@misc{graph,
    author = "{蓮尾 一郎}",
    pagetitle = "{モデル検査入門}",
    year = {2009},
    URL = {http://www.kurims.kyoto-u.ac.jp/~cs/lecture2009/lecture09ModelChecking.pdf},}