@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 Reflection-Refarence                  
@article{weko_5056_1,
   author	 = "菅野,博靖 and 田中,二郎",
   title	 = "非標準理論とその応用：メタ推論とリフレクション",
   journal	 = "情報処理",
   year 	 = "1989",
   volume	 = "30",
   number	 = "6",
   month	 = "jun"
}

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


@misc{agda,
    title = {The Agda wiki},
    howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
    note = {Accessed: 2018/2/9(Fri)}
}

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

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

@misc{spin,
    title = {Spin - Formal Verification},
    howpublished = {\url{http://spinroot.com/spin/whatispin.html}},
    note = {Accessed: 2018/02/09(Fri)}
}

@misc{nusmv,
    title = {NuSMV home page},
    howpublished = {\url{http://nusmv.fbk.eu/}},
    note = {Accessed: 2018/02/09(Fri)}
}

@misc{cbmc,
    title = {The CBMC Homepage},
    howpublished = {\url{http://www.cprover.org/cbmc/}},
    note = {Accessed: 2018/02/09(Fri)}
}


@phdthesis{norell:thesis,
  author  = {Ulf Norell},
  title	  = {Towards a practical programming language based on dependent type
	     theory},
  school  = {Department of Computer Science and Engineering, Chalmers University of Technology},
  year	  = 2007,
  month	  = {September},
  address = {SE-412 96 G\"{o}teborg, Sweden}
}

@Comment attomisc{agda-tutorial,
@Comment     title = {agda-tutorial},
@Comment     howpublished = {\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}},
@Comment }
@Comment \bibtem{Agda-Tutorial}
@Comment % {Ulf Norell and James Chapman}: Dependently Typed Programming in Agda
@Comment % \\\verb|http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf|
                  
@misc{agda-documentation,
    title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation},
    howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}},
    note = {Accessed: 2018/2/9(Fri)}
}

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


@Comment Hoare-Reference

@article{Hoare1969AnAB,
  title={An Axiomatic Basis for Computer Programming},
  author={C. A. R. Hoare},
  journal={Commun. ACM},
  year={1969},
  volume={12},
  pages={576-580}
}

@book{Girard:1989:PT:64805,
 author    = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
 title     = {Proofs and Types},
 year      = {1989},
 isbn      = {0-521-37181-3},
 publisher = {Cambridge University Press},
 address   = {New York, NY, USA},
}