|
1
|
1 @techreport{ryokka-sigos,
|
|
|
2 author = "外間,政尊 and 河野,真治",
|
|
|
3 title = "GearsOSのAgdaによる記述と検証",
|
|
|
4 year = "2018",
|
|
|
5 institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
|
|
|
6 number = "5",
|
|
|
7 month = "may"
|
|
|
8 }
|
|
|
9
|
|
|
10 @misc{agda-wiki,
|
|
|
11 title = {The Agda wiki},
|
|
|
12 howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
|
|
|
13 }
|
|
|
14
|
|
|
15 @book{Stump:2016:VFP:2841316,
|
|
|
16 author = {Stump, Aaron},
|
|
|
17 title = {Verified Functional Programming in Agda},
|
|
|
18 year = {2016},
|
|
|
19 isbn = {978-1-97000-127-3},
|
|
|
20 publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool},
|
|
|
21 address = {New York, NY, USA},
|
|
|
22 }
|
|
|
23
|
|
|
24 @mastersthesis{atton-master,
|
|
|
25 author = "比嘉健太",
|
|
|
26 title = "メタ計算を用いた Continuation based C の検証手法",
|
|
|
27 school = "琉球大学 大学院理工学研究科 情報工学専攻",
|
|
|
28 year = "2017"
|
|
|
29 }
|
|
|
30
|
|
|
31 @mastersthesis{parusu-master,
|
|
|
32 author = "伊波立樹",
|
|
|
33 title = "Gears OS の並列処理",
|
|
|
34 school = "琉球大学 大学院理工学研究科 情報工学専攻",
|
|
|
35 year = "2018"
|
|
|
36 }
|
|
|
37
|
|
|
38 @article{kaito-lola,
|
|
|
39 author = "Kaito, Tokumori and Shinji, Kono",
|
|
|
40 title = "Implementing Continuation based language in LLVM and Clang",
|
|
|
41 journal = "LOLA 2015, Kyoto",
|
|
|
42 month = "July",
|
|
|
43 year = 2015
|
|
|
44
|
|
|
45 }
|
|
|
46 @article{hoare,
|
|
|
47 author = {Hoare, C. A. R.},
|
|
|
48 title = {An Axiomatic Basis for Computer Programming},
|
|
|
49 year = {1969},
|
|
|
50 issue_date = {October 1969},
|
|
|
51 publisher = {Association for Computing Machinery},
|
|
|
52 address = {New York, NY, USA},
|
|
|
53 volume = {12},
|
|
|
54 number = {10},
|
|
|
55 issn = {0001-0782},
|
|
|
56 url = {https://doi.org/10.1145/363235.363259},
|
|
|
57 doi = {10.1145/363235.363259},
|
|
|
58 journal = {Commun. ACM},
|
|
|
59 month = oct,
|
|
|
60 pages = {576–580},
|
|
|
61 numpages = {5},
|
|
|
62 keywords = {programming language design, theory of programming’ proofs of programs, machine-independent programming, program documentation, axiomatic method, formal language definition}
|
|
|
63 }
|
|
14
|
64
|
|
|
65 @inproceedings{agda,
|
|
|
66 author = {Norell, Ulf},
|
|
|
67 title = {Dependently Typed Programming in Agda},
|
|
|
68 booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
|
|
|
69 series = {TLDI '09},
|
|
|
70 year = {2009},
|
|
|
71 isbn = {978-1-60558-420-1},
|
|
|
72 location = {Savannah, GA, USA},
|
|
|
73 pages = {1--2},
|
|
|
74 numpages = {2},
|
|
|
75 url = {http://doi.acm.org/10.1145/1481861.1481862},
|
|
|
76 doi = {10.1145/1481861.1481862},
|
|
|
77 acmid = {1481862},
|
|
|
78 publisher = {ACM},
|
|
|
79 address = {New York, NY, USA},
|
|
|
80 keywords = {dependent types, programming},
|
|
|
81 }
|
|
|
82
|
|
|
83 @misc{agda2-hoare,
|
|
|
84 title = {Hoare Logic in Agda2},
|
|
|
85 howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}},
|
|
|
86 note = {Accessed: 2020/2/9(Sun)},
|
|
|
87 }
|
|
|
88
|
|
|
89 @misc{cr-ryukyu,
|
|
|
90 title = {Hoare Logic - 並列信頼研 mercurial repository},
|
|
|
91 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/}},
|
|
|
92 note = {Accessed: 2020/2/9(Sun)}
|
|
|
93 }
|
|
|
94
|
|
|
95 @misc{cbc-gcc,
|
|
|
96 title = {cbc-gcc - 並列信頼研 mercurial repository},
|
|
|
97 howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}},
|
|
|
98 note = {Accessed: 2020/2/9(Sun)}
|
|
|
99 }
|
|
|
100
|
|
|
101 @inproceedings{mitsuki-prosym,
|
|
|
102 author = "宮城光希 and 河野真治",
|
|
17
|
103 title = "CodeGear と DataGear を持つ Gears OS の設計",
|
|
14
|
104 booktitle = "第59回プログラミング・シンポジウム予稿集",
|
|
|
105 year = "2018",
|
|
|
106 volume = "2018",
|
|
|
107 pages = "197--206",
|
|
|
108 month = "jan"
|
|
|
109 }
|
|
|
110
|
|
|
111 @mastersthesis{ikkun-master,
|
|
|
112 author = "東恩納 琢偉",
|
|
|
113 title = "Gears OS でモデル検査を実現する方法について",
|
|
|
114 school = "琉球大学 大学院理工学研究科 情報工学専攻",
|
|
|
115 year = "2021"
|
|
|
116 }
|
|
|
117
|
|
|
118 @inproceedings{EdmundM,
|
|
|
119 author = "{Edmund M. Clarke, Jr}",
|
|
|
120 booktitle = "{Model Checking, Second Edition}",
|
|
|
121 year = {2018},}
|
|
|
122
|
|
|
123 @misc{spin,
|
|
|
124 title = {Spin - Formal Verification},
|
|
|
125 howpublished = {\url{http://spinroot.com/}},
|
|
|
126 note = {Accessed: 2023/2/1(Wed)},
|
|
|
127 }
|
|
|
128
|
|
|
129
|
|
|
130 @misc{agda-stdlib,
|
|
|
131 title = {agda-stdlib},
|
|
|
132 howpublished = {\url{https://github.com/agda/agda-stdlib
|
|
|
133 }},
|
|
|
134 note = {Accessed: 2023/2/1(Wed)},
|
|
|
135 }
|
|
|
136
|
|
|
137 @misc{rbtree,
|
|
|
138 title={データ構造と基本アルゴリズム},
|
|
|
139 author={渡邉},
|
|
|
140 year={2000},
|
|
|
141 publisher={共立出版}
|
|
|
142 }
|
|
|
143
|
|
|
144 @misc{model,
|
|
|
145 title={コンピュータ基礎理論ハンドブック 形式的モデルと意味論},
|
|
|
146 author={広瀬健},
|
|
|
147 year={1994},
|
|
|
148 publisher={丸善出版}
|
|
|
149 }
|
|
|
150
|
