@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 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/4/23(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} } @article{ek2009formalizing, title={Formalizing Arne Andersson trees and left-leaning Red-Black trees in Agda}, author={Ek, Linus and Holmstr{\"o}m, Ola and Andjelkovic, Stevan} } @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 latest documentation}, howpublished = {\url{http://agda.readthedocs.io/en/latest/}}, note = {Accessed: 2018/4/23(Mon)} } @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}, }