|
0
|
1 @inproceedings{agda,
|
|
|
2 author = {Norell, Ulf},
|
|
|
3 title = {Dependently Typed Programming in Agda},
|
|
|
4 booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
|
|
|
5 series = {TLDI '09},
|
|
|
6 year = {2009},
|
|
|
7 isbn = {978-1-60558-420-1},
|
|
|
8 location = {Savannah, GA, USA},
|
|
|
9 pages = {1--2},
|
|
|
10 numpages = {2},
|
|
|
11 url = {http://doi.acm.org/10.1145/1481861.1481862},
|
|
|
12 doi = {10.1145/1481861.1481862},
|
|
|
13 acmid = {1481862},
|
|
|
14 publisher = {ACM},
|
|
|
15 address = {New York, NY, USA},
|
|
|
16 keywords = {dependent types, programming},
|
|
|
17 }
|
|
|
18
|
|
|
19
|
|
|
20 @article{atton-ipsj,
|
|
|
21 author="比嘉 健太 and 河野 真治",
|
|
|
22 title="Verification Method of Programs Using Continuation based C",
|
|
|
23 journal="情報処理学会論文誌プログラミング（PRO）",
|
|
|
24 ISSN="1882-7802",
|
|
|
25 publisher="",
|
|
|
26 year="2017",
|
|
|
27 month="feb",
|
|
|
28 volume="10",
|
|
|
29 number="2",
|
|
|
30 pages="5-5",
|
|
|
31 URL="https://ci.nii.ac.jp/naid/170000148438/en/",
|
|
|
32 DOI="",
|
|
|
33 }
|
|
|
34
|
|
|
35 @article{moggi-monad,
|
|
|
36 author = {Moggi, Eugenio},
|
|
|
37 title = {Notions of Computation and Monads},
|
|
|
38 journal = {Inf. Comput.},
|
|
|
39 issue_date = {July 1991},
|
|
|
40 volume = {93},
|
|
|
41 number = {1},
|
|
|
42 month = jul,
|
|
|
43 year = {1991},
|
|
|
44 issn = {0890-5401},
|
|
|
45 pages = {55--92},
|
|
|
46 numpages = {38},
|
|
|
47 url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
|
|
|
48 doi = {10.1016/0890-5401(91)90052-4},
|
|
|
49 acmid = {116984},
|
|
|
50 publisher = {Academic Press, Inc.},
|
|
|
51 address = {Duluth, MN, USA},
|
|
|
52 }
|
|
|
53
|
|
|
54 @inproceedings{mitsuki-prosym,
|
|
|
55 author = "宮城光希 and 河野真治",
|
|
|
56 title = "Code Gear と Data Gear を持つ Gears OS の設計",
|
|
|
57 booktitle = "第59回プログラミング・シンポジウム予稿集",
|
|
|
58 year = "2018",
|
|
|
59 volume = "2018",
|
|
|
60 pages = "197--206",
|
|
|
61 month = "jan"
|
|
|
62 }
|
|
|
63
|
|
|
64
|
|
|
65 @techreport{ryokka-sigos,
|
|
|
66 author = "外間,政尊 and 河野,真治",
|
|
|
67 title = "GearsOSのAgdaによる記述と検証",
|
|
|
68 year = "2018",
|
|
|
69 institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
|
|
|
70 number = "5",
|
|
|
71 month = "may"
|
|
|
72 }
|
|
|
73
|
|
|
74 @misc{agda-wiki,
|
|
|
75 title = {The Agda wiki},
|
|
|
76 howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
|
|
|
77 note = {Accessed: 2018/12/17(Mon)},
|
|
|
78 }
|
|
|
79
|
|
|
80
|
|
|
81 @misc{agda-documentation,
|
|
|
82 title = {Welcome to Agda’s documentation! — Agda latest documentation},
|
|
|
83 howpublished = {\url{http://agda.readthedocs.io/en/latest/}},
|
|
|
84 note = {Accessed: 2018/12/17(Mon)},
|
|
|
85 }
|
|
|
86
|
|
|
87 @book{Stump:2016:VFP:2841316,
|
|
|
88 author = {Stump, Aaron},
|
|
|
89 title = {Verified Functional Programming in Agda},
|
|
|
90 year = {2016},
|
|
|
91 isbn = {978-1-97000-127-3},
|
|
|
92 publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool},
|
|
|
93 address = {New York, NY, USA},
|
|
|
94 }
|
|
|
95
|
|
|
96 @article{10.1145/363235.363259,
|
|
|
97 author = {Hoare, C. A. R.},
|
|
|
98 title = {An Axiomatic Basis for Computer Programming},
|
|
|
99 year = {1969},
|
|
|
100 issue_date = {October 1969},
|
|
|
101 publisher = {Association for Computing Machinery},
|
|
|
102 address = {New York, NY, USA},
|
|
|
103 volume = {12},
|
|
|
104 number = {10},
|
|
|
105 issn = {0001-0782},
|
|
|
106 url = {https://doi.org/10.1145/363235.363259},
|
|
|
107 doi = {10.1145/363235.363259},
|
|
|
108 journal = {Commun. ACM},
|
|
|
109 month = oct,
|
|
|
110 pages = {576–580},
|
|
|
111 numpages = {5},
|
|
|
112 keywords = {programming language design, theory of programming’ proofs of programs, machine-independent programming, program documentation, axiomatic method, formal language definition}
|
|
|
113 }
|
|
|
114
|
|
|
115
|
|
|
116 @misc{agda-alpa-old,
|
|
|
117 title = {Example - Hoare Logic},
|
|
|
118 howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}},
|
|
|
119 note = {Accessed: 2019/1/16(Wed)},
|
|
|
120 }
|
|
|
121
|
|
|
122 @misc{agda-alpa,
|
|
|
123 title = {Agda1},
|
|
|
124 howpublished = {\url{https://sourceforge.net/projects/agda/}},
|
|
|
125 note = {Accessed: 2020/2/9(Sun)},
|
|
|
126 }
|
|
|
127
|
|
|
128 @misc{agda2-hoare,
|
|
|
129 title = {Hoare Logic in Agda2},
|
|
|
130 howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}},
|
|
|
131 note = {Accessed: 2020/2/9(Sun)},
|
|
|
132 }
|
|
|
133
|
|
|
134 @misc{coq-old,
|
|
|
135 title = {Welcome! | The Coq Proof Assistant},
|
|
|
136 howpublished = {\url{https://coq.inria.fr/}},
|
|
|
137 note = {Accessed: 2020/2/9(Sun)},
|
|
|
138 }
|
|
|
139
|
|
|
140
|
|
|
141 @misc{coq,
|
|
|
142 title = {Coq Source},
|
|
|
143 howpublished = {\url{https://github.com/coq/coq}},
|
|
|
144 note = {Accessed: 2020/2/9(Sun)},
|
|
|
145 }
|
|
|
146
|
|
|
147
|
|
|
148 @misc{ats2,
|
|
|
149 title = {ATS-PL-SYS},
|
|
|
150 howpublished = {\url{http://www.ats-lang.org/}},
|
|
|
151 note = {Accessed: 2020/2/9(Sun)},
|
|
|
152 }
|
|
|
153
|
|
|
154 @misc{rust,
|
|
|
155 title = {Rust programming language},
|
|
|
156 howpublished = {\url{https://www.rust-lang.org/}},
|
|
|
157 note = {Accessed: 2020/2/9(Sun)},
|
|
|
158 }
|
|
|
159
|
|
|
160
|
|
|
161 @article{Klein:2010:SFV:1743546.1743574,
|
|
|
162 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},
|
|
|
163 title = {seL4: Formal Verification of an Operating-system Kernel},
|
|
|
164 journal = {Commun. ACM},
|
|
|
165 issue_date = {June 2010},
|
|
|
166 volume = {53},
|
|
|
167 number = {6},
|
|
|
168 month = jun,
|
|
|
169 year = {2010},
|
|
|
170 issn = {0001-0782},
|
|
|
171 pages = {107--115},
|
|
|
172 numpages = {9},
|
|
|
173 url = {http://doi.acm.org/10.1145/1743546.1743574},
|
|
|
174 doi = {10.1145/1743546.1743574},
|
|
|
175 acmid = {1743574},
|
|
|
176 publisher = {ACM},
|
|
|
177 address = {New York, NY, USA},
|
|
|
178 }
|
|
|
179
|
|
|
180 @inproceedings{Nelson:2017:HPV:3132747.3132748,
|
|
|
181 author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi},
|
|
|
182 title = {Hyperkernel: Push-Button Verification of an OS Kernel},
|
|
|
183 booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles},
|
|
|
184 series = {SOSP '17},
|
|
|
185 year = {2017},
|
|
|
186 isbn = {978-1-4503-5085-3},
|
|
|
187 location = {Shanghai, China},
|
|
|
188 pages = {252--269},
|
|
|
189 numpages = {18},
|
|
|
190 url = {http://doi.acm.org/10.1145/3132747.3132748},
|
|
|
191 doi = {10.1145/3132747.3132748},
|
|
|
192 acmid = {3132748},
|
|
|
193 publisher = {ACM},
|
|
|
194 address = {New York, NY, USA},
|
|
|
195 }
|
|
|
196
|
|
|
197 @misc{cr-ryukyu,
|
|
|
198 title = {whileTestPrim.agda - 並列信頼研 mercurial repository},
|
|
|
199 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda}},
|
|
|
200 note = {Accessed: 2020/2/9(Sun)}
|
|
|
201 }
|
|
|
202
|
|
|
203 @mastersthesis{utah-master,
|
|
|
204 author = "徳森海斗",
|
|
|
205 title = "LLVM Clang 上の Continuation based C コンパイラ の改良",
|
|
|
206 school = "琉球大学 大学院理工学研究科 情報工学専攻",
|
|
|
207 year = "2016"
|
|
|
208 }
|
|
|
209
|
|
|
210 @mastersthesis{atton-master,
|
|
|
211 author = "比嘉健太",
|
|
|
212 title = "メタ計算を用いた Continuation based C の検証手法",
|
|
|
213 school = "琉球大学 大学院理工学研究科 情報工学専攻",
|
|
|
214 year = "2017"
|
|
|
215 }
|
|
|
216
|
|
|
217 @mastersthesis{parusu-master,
|
|
|
218 author = "伊波立樹",
|
|
|
219 title = "Gears OS の並列処理",
|
|
|
220 school = "琉球大学 大学院理工学研究科 情報工学専攻",
|
|
|
221 year = "2018"
|
|
|
222 }
|
|
|
223
|
|
|
224 @mastersthesis{mitsuki-master,
|
|
|
225 author = "宮城光希",
|
|
|
226 title = "継続を基本とした言語による OS のモジュール化",
|
|
|
227 school = "琉球大学 大学院理工学研究科 情報工学専攻",
|
|
|
228 year = "2019"
|
|
|
229 }
|
|
|
230
|
|
|
231 @inproceedings{weko_82695_1,
|
|
|
232 author = "大城,信康 and 河野,真治",
|
|
|
233 title = "Continuation based C の GCC4.6 上の実装について",
|
|
|
234 booktitle = "第53回プログラミング・シンポジウム予稿集",
|
|
|
235 year = "2012",
|
|
|
236 volume = "2012",
|
|
|
237 number = "",
|
|
|
238 pages = "69--78",
|
|
|
239 month = "jan"
|
|
|
240 }
|
|
|
241
|
|
|
242 @article{kaito-lola,
|
|
|
243 author = "Kaito, Tokumori and Shinji, Kono",
|
|
|
244 title = "Implementing Continuation based language in LLVM and Clang",
|
|
|
245 journal = "LOLA 2015, Kyoto",
|
|
|
246 month = "July",
|
|
|
247 year = 2015
|
|
|
248
|
|
|
249 }
|
|
|
250
|
|
|
251
|
|
|
252 @misc{cbc-llvm,
|
|
|
253 title = {cbc-llvm - 並列信頼研 mercurial repository},
|
|
|
254 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}},
|
|
|
255 note = {Accessed: 2020/2/9(Sun)}
|
|
|
256 }
|
|
|
257
|
|
|
258 @misc{cbc-gcc,
|
|
|
259 title = {cbc-gcc - 並列信頼研 mercurial repository},
|
|
|
260 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}},
|
|
|
261 note = {Accessed: 2020/2/9(Sun)}
|
|
|
262 }
|
|
|
263
|
|
|
264
|
|
|
265 @misc{loop-proof,
|
|
|
266 title = {loopSemInduct - 並列信頼研 mercurial repository},
|
|
|
267 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestGears.agda}},
|
|
|
268 note = {Accessed: 2020/2/9(Sun)}
|
|
|
269 }
|
|
|
270
|
