|
7
|
1 @article{
|
|
|
2 gears,
|
|
|
3 author = "河野 真治 and 伊波 立樹 and 東恩納 琢偉",
|
|
|
4 title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
|
|
|
5 journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
|
|
|
6 month = "May",
|
|
|
7 year = 2016
|
|
|
8 }
|
|
|
9
|
|
|
10 @article{
|
|
|
11 cbc,
|
|
|
12 author = "Kaito TOKKMORI and Shinji KONO",
|
|
|
13 title = "Implementing Continuation based language in LLVM and Clang",
|
|
|
14 journal = "LOLA 2015",
|
|
|
15 month = "July",
|
|
|
16 year = 2015
|
|
|
17 }
|
|
|
18
|
|
|
19 @Misc{mitsuki:2017,
|
|
|
20 author = "{宮城 光希, 河野 真治}",
|
|
|
21 title = "{CbC 言語による OS 記述}",
|
|
|
22 journal = "{琉球大学工学部情報工学科平成 29 年度学位論文}",
|
|
|
23 year = 2017
|
|
|
24 }
|
|
|
25
|
|
|
26 @Comment Agda-Reference
|
|
|
27
|
|
|
28 @article{170000148438,
|
|
|
29 author="比嘉, 健太 and 河野, 真治",
|
|
|
30 title="Verification Method of Programs Using Continuation based C",
|
|
|
31 journal="情報処理学会論文誌プログラミング（PRO）",
|
|
|
32 ISSN="1882-7802",
|
|
|
33 publisher="",
|
|
|
34 year="2017",
|
|
|
35 month="feb",
|
|
|
36 volume="10",
|
|
|
37 number="2",
|
|
|
38 pages="5-5",
|
|
|
39 URL="https://ci.nii.ac.jp/naid/170000148438/en/",
|
|
|
40 DOI="",
|
|
|
41 }
|
|
|
42
|
|
|
43
|
|
|
44 @techreport{ryokka-sigos,
|
|
|
45 author = "外間,政尊 and 河野,真治",
|
|
|
46 title = "GearsOSのAgdaによる記述と検証",
|
|
|
47 year = "2018",
|
|
|
48 institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
|
|
|
49 number = "5",
|
|
|
50 month = "may"
|
|
|
51 }
|
|
|
52
|
|
|
53 @misc{agda,
|
|
|
54 title = {The Agda wiki},
|
|
|
55 howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
|
|
|
56 note = {Accessed: 2018/12/17(Mon)}
|
|
|
57 }
|
|
|
58
|
|
|
59
|
|
|
60 @misc{agda-documentation,
|
|
|
61 title = {Welcome to Agda’s documentation! — Agda latest documentation},
|
|
|
62 howpublished = {\url{http://agda.readthedocs.io/en/latest/}},
|
|
|
63 note = {Accessed: 2018/12/17(Mon)}
|
|
|
64 }
|
|
|
65
|
|
|
66 @book{Stump:2016:VFP:2841316,
|
|
|
67 author = {Stump, Aaron},
|
|
|
68 title = {Verified Functional Programming in Agda},
|
|
|
69 year = {2016},
|
|
|
70 isbn = {978-1-97000-127-3},
|
|
|
71 publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool},
|
|
|
72 address = {New York, NY, USA},
|
|
|
73 }
|
|
|
74
|
|
|
75
|
|
8
|
76 @misc{agda-alpa,
|
|
7
|
77 title = {Example - Hoare Logic},
|
|
|
78 howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}},
|
|
|
79 note = {Accessed: 2018/12/17(Mon)}
|
|
|
80 }
|
|
|
81
|
|
|
82 @misc{agda2-hoare,
|
|
|
83 title = {Hoare Logic in Agda2},
|
|
|
84 howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}},
|
|
|
85 note = {Accessed: 2018/12/17(Mon)}
|
|
|
86 }
|
|
|
87
|
|
|
88
|
|
|
89
|
|
|
90 @article{Klein:2010:SFV:1743546.1743574,
|
|
|
91 author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Heiser, Gernot 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},
|
|
|
92 title = {seL4: Formal Verification of an Operating-system Kernel},
|
|
|
93 journal = {Commun. ACM},
|
|
|
94 issue_date = {June 2010},
|
|
|
95 volume = {53},
|
|
|
96 number = {6},
|
|
|
97 month = jun,
|
|
|
98 year = {2010},
|
|
|
99 issn = {0001-0782},
|
|
|
100 pages = {107--115},
|
|
|
101 numpages = {9},
|
|
|
102 url = {http://doi.acm.org/10.1145/1743546.1743574},
|
|
|
103 doi = {10.1145/1743546.1743574},
|
|
|
104 acmid = {1743574},
|
|
|
105 publisher = {ACM},
|
|
|
106 address = {New York, NY, USA},
|
|
|
107 }
|
|
|
108
|
|
|
109 @inproceedings{Nelson:2017:HPV:3132747.3132748,
|
|
|
110 author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi},
|
|
|
111 title = {Hyperkernel: Push-Button Verification of an OS Kernel},
|
|
|
112 booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles},
|
|
|
113 series = {SOSP '17},
|
|
|
114 year = {2017},
|
|
|
115 isbn = {978-1-4503-5085-3},
|
|
|
116 location = {Shanghai, China},
|
|
|
117 pages = {252--269},
|
|
|
118 numpages = {18},
|
|
|
119 url = {http://doi.acm.org/10.1145/3132747.3132748},
|
|
|
120 doi = {10.1145/3132747.3132748},
|
|
|
121 acmid = {3132748},
|
|
|
122 publisher = {ACM},
|
|
|
123 address = {New York, NY, USA},
|
|
|
124 }
|
|
|
125
|
|
|
126 @misc{cr-ryukyu,
|
|
|
127 title = {whileTestPrim.agda - 並列信頼研 mercurial repository},
|
|
|
128 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda}},
|
|
|
129 note = {Accessed: 2018/12/17(Mon)}
|
|
|
130 } |
