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

@book{opac-b1092711,
   title = "Introduction to higher order categorical logic",
   author = "Lambek, Joachim (mathématicien) and Scott, P. J.",
   series = "Cambridge studies in advanced mathematics",
   publisher = "Cambridge University Press",
   address = "Cambridge, New York (N. Y.), Melbourne",
   url = "http://opac.inria.fr/record=b1092711",
   isbn = "0-521-24665-2",
   year = 1986
}

@book{BarrM:cattcs,
    author    = {Barr, Michael and Wells, Charles},
    title     = {Category Theory for Computing Science},
    publisher = {Prentice-Hall},
    series    = {International Series in Computer Science},
    year      = 1990,
    note      = {Second edition, 1995},
    isbn      = {0-13-120486-6},
    lccn      = {QA76.9.M35B37 1990}
}

@article{Moggi:1991:NCM:116981.116984,
    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},
}

@techreport{JonesDuponcheel93,
  author      = {M. P. Jones and L. Duponcheel},
  title       = {Composing monads},
  institution = {Yale University},
  year        = {1993},
  month       = {December},
  number      = {YALEU/DCS/RR-1004},
  type        = {Research Report},
  ftp         = {ftp://ftp.cs.nott.ac.uk/nott-fp/reports/yale/RR-1004.ps}
}

@article{110009766999,
author="Kaito, Tokumori and Shinji, Kono",
title="The implementation of Continuation based C Compiler on LLVM/clang 3.5",
journal="IPSJ SIG Notes",
ISSN="",
publisher="Information Processing Society of Japan (IPSJ)",
year="2014",
month="may",
volume="2014",
number="10",
pages="1-11",
URL="http://ci.nii.ac.jp/naid/110009766999/en/",
DOI="",
}

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

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

@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: 2016/01/31(Tue)}
}



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

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

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

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

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

@misc{opencl,
    title = {OpenCL | NVIDIA Developer},
    howpublished = {\url{https://developer.nvidia.com/opencl}},
    note = {Accessed: 2016/02/06(Mon)}
}

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



@techreport{weko_142109_1,
   author      = "小久保,翔平 and 伊波,立樹 and 河野,真治",
   title       = "Monadに基づくメタ計算を基本とするGears OSの設計",
   year        = "2015",
   institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科, 琉球大学工学部情報工学科",
   number      = "16",
   month       = "may"
}

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

@misc{atton-ipsjpro,
    author = "比嘉 健太, 河野 真治",
    title  = "Continuation based C を用いたプログラムの検証手法",
}

@book{Pierce:2002:TPL:509043,
    author = {Pierce, Benjamin C.},
    title = {Types and Programming Languages},
    year = {2002},
    isbn = {0262162091, 9780262162098},
    edition = {1st},
    publisher = {The MIT Press},
}

@book{pierce2013型システム入門プログラミング言語と型の理論,
  title={型システム入門プログラミング言語と型の理論: },
  author={Pierce, B.C.},
  isbn={9784274069116},
  url={https://books.google.co.jp/books?id=Sx8UmwEACAAJ},
  year={2013},
  publisher={オーム社}
}

@inproceedings{Norell:2009:DTP:1481861.1481862,
 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{Backus:1978:HFI:960118.808380,
 author = {Backus, John},
 title = {The History of FORTRAN I, II, and III},
 journal = {SIGPLAN Not.},
 issue_date = {August 1978},
 volume = {13},
 number = {8},
 month = aug,
 year = {1978},
 issn = {0362-1340},
 pages = {165--180},
 numpages = {16},
 url = {http://doi.acm.org/10.1145/960118.808380},
 doi = {10.1145/960118.808380},
 acmid = {808380},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@ARTICLE{Landin64,
  AUTHOR = {Peter J. Landin},
  TITLE = {The Mechanical Evaluation of Expressions},
  JOURNAL = {Computer Journal},
  VOLUME = 6,
  NUMBER = 4,
  MONTH = JAN,
  YEAR = 1964,
  PAGES = {308--320},
  CHECKED = {5 June 1992, by JCR}
}
@book{GlossarWiki:Church:1941,
   author = {Church, Alonzo},
   title = {The Calculi of Lambda-Conversion},
   publisher = {Princeton University Press},
   year = {1941},
   address = {Princeton, New Jork},
   url = {http://books.google.de/books/about/The_Calculi_of_Lambda_conversion.html?id=KCOuGztKVgcC},
   quality = {5},
   note = {}
 }

@article{haskell-sigplan
    ,author="Hudak, P. and Peyton Jones, S. and Wadler (editors), P."
    ,title="Report on the {P}rogramming {L}anguage {H}askell,
           {A} {N}on-strict {P}urely {F}unctional {L}anguage ({V}ersion 1.2)"
    ,journal="ACM SIGPLAN Notices"
    ,volume=27
    ,number=5
    ,month=May
    ,year=1992
    }

@article{DEBRUIJN1972381,
title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
journal = "Indagationes Mathematicae (Proceedings)",
volume = "75",
number = "5",
pages = "381 - 392",
year = "1972",
note = "",
issn = "1385-7258",
doi = "http://dx.doi.org/10.1016/1385-7258(72)90034-0",
url = "http://www.sciencedirect.com/science/article/pii/1385725872900340",
author = "N.G de Bruijn",

}