Mercurial > hg > Papers > 2017 > atton-master
annotate paper/reference.bib @ 106:cc2ca280345f
Fix cover
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 13 Feb 2017 13:22:18 +0900 |
parents | 16dc3337a5a9 |
children | 18f872806bc0 |
rev | line source |
---|---|
6
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 @book{Girard:1989:PT:64805, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 title = {Proofs and Types}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 year = {1989}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 isbn = {0-521-37181-3}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 publisher = {Cambridge University Press}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 address = {New York, NY, USA}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 } |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 @book{opac-b1092711, |
12 | 11 title = "Introduction to higher order categorical logic", |
12 author = "Lambek, Joachim (mathématicien) and Scott, P. J.", | |
13 series = "Cambridge studies in advanced mathematics", | |
6
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 publisher = "Cambridge University Press", |
12 | 15 address = "Cambridge, New York (N. Y.), Melbourne", |
16 url = "http://opac.inria.fr/record=b1092711", | |
17 isbn = "0-521-24665-2", | |
18 year = 1986 | |
6
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 } |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 @book{BarrM:cattcs, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 author = {Barr, Michael and Wells, Charles}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 title = {Category Theory for Computing Science}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 publisher = {Prentice-Hall}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 series = {International Series in Computer Science}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 year = 1990, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 note = {Second edition, 1995}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 isbn = {0-13-120486-6}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 lccn = {QA76.9.M35B37 1990} |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 } |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 @article{Moggi:1991:NCM:116981.116984, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 author = {Moggi, Eugenio}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 title = {Notions of Computation and Monads}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 journal = {Inf. Comput.}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 issue_date = {July 1991}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 volume = {93}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 number = {1}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 month = jul, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 year = {1991}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 issn = {0890-5401}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 pages = {55--92}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 numpages = {38}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 doi = {10.1016/0890-5401(91)90052-4}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 acmid = {116984}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 publisher = {Academic Press, Inc.}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 address = {Duluth, MN, USA}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 } |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 @techreport{JonesDuponcheel93, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 author = {M. P. Jones and L. Duponcheel}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 title = {Composing monads}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 institution = {Yale University}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 year = {1993}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 month = {December}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 number = {YALEU/DCS/RR-1004}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 type = {Research Report}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 ftp = {ftp://ftp.cs.nott.ac.uk/nott-fp/reports/yale/RR-1004.ps} |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 } |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 |
12 | 62 @article{110009766999, |
63 author="Kaito, Tokumori and Shinji, Kono", | |
64 title="The implementation of Continuation based C Compiler on LLVM/clang 3.5", | |
65 journal="IPSJ SIG Notes", | |
66 ISSN="", | |
67 publisher="Information Processing Society of Japan (IPSJ)", | |
68 year="2014", | |
69 month="may", | |
70 volume="2014", | |
71 number="10", | |
72 pages="1-11", | |
73 URL="http://ci.nii.ac.jp/naid/110009766999/en/", | |
74 DOI="", | |
75 } | |
76 | |
77 @inproceedings{weko_82695_1, | |
78 author = "大城,信康 and 河野,真治", | |
79 title = "Continuation based C の GCC4.6 上の実装について", | |
80 booktitle = "第53回プログラミング・シンポジウム予稿集", | |
81 year = "2012", | |
82 volume = "2012", | |
83 number = "", | |
84 pages = "69--78", | |
85 month = "jan" | |
86 } | |
87 | |
6
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 @misc{agda, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 title = {The Agda wiki}, |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, |
20 | 91 note = {Accessed: 2016/01/20(Fri)} |
92 } | |
93 | |
52 | 94 @misc{agda-documentation, |
95 title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation}, | |
96 howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}}, | |
97 note = {Accessed: 2016/01/31(Tue)} | |
98 } | |
99 | |
100 | |
101 | |
20 | 102 @misc{coq, |
103 title = {Welcome! | The Coq Proof Assistant}, | |
104 howpublished = {\url{https://coq.inria.fr/}}, | |
105 note = {Accessed: 2016/01/20(Fri)} | |
106 } | |
107 | |
108 @misc{ats2, | |
109 title = {ATS-PL-SYS}, | |
110 howpublished = {\url{http://www.ats-lang.org/}}, | |
111 note = {Accessed: 2016/01/20(Fri)} | |
6
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 } |
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 |
20 | 114 @misc{spin, |
115 title = {Spin - Formal Verification}, | |
116 howpublished = {\url{http://spinroot.com/spin/whatispin.html}}, | |
117 note = {Accessed: 2016/01/20(Fri)} | |
118 } | |
119 | |
120 @misc{nusmv, | |
121 title = {NuSMV home page}, | |
122 howpublished = {\url{http://nusmv.fbk.eu/}}, | |
123 note = {Accessed: 2016/01/20(Fri)} | |
124 } | |
125 | |
126 @misc{cbmc, | |
127 title = {The CBMC Homepage}, | |
128 howpublished = {\url{http://www.cprover.org/cbmc/}}, | |
129 note = {Accessed: 2016/01/20(Fri)} | |
130 } | |
131 | |
74 | 132 @misc{opencl, |
133 title = {OpenCL | NVIDIA Developer}, | |
134 howpublished = {\url{https://developer.nvidia.com/opencl}}, | |
135 note = {Accessed: 2016/02/06(Mon)} | |
136 } | |
137 | |
138 @misc{cuda, | |
139 title = {CUDA Zone | NVIDIA Developer}, | |
140 howpublished = {\url{https://developer.nvidia.com/cuda-zone}}, | |
141 note = {Accessed: 2016/02/06(Mon)} | |
142 } | |
143 | |
20 | 144 |
145 | |
17 | 146 @techreport{weko_142109_1, |
18 | 147 author = "小久保,翔平 and 伊波,立樹 and 河野,真治", |
148 title = "Monadに基づくメタ計算を基本とするGears OSの設計", | |
149 year = "2015", | |
150 institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科, 琉球大学工学部情報工学科", | |
151 number = "16", | |
152 month = "may" | |
17 | 153 } |
154 | |
23 | 155 @mastersthesis{utah-master, |
156 author = "徳森海斗", | |
157 title = "LLVM Clang 上の Continuation based C コンパイラ の改良", | |
158 school = "琉球大学 大学院理工学研究科 情報工学専攻", | |
159 year = "2016" | |
160 } | |
93 | 161 |
162 @mastersthesis{kkb-master, | |
163 author = "小久保 翔平", | |
164 title = "Code Segment と Data Segment を持つ Gears OS の 設計", | |
165 school = "琉球大学 大学院理工学研究科 情報工学専攻", | |
166 year = "2016" | |
167 } | |
168 | |
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
169 @book{Pierce:2002:TPL:509043, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
170 author = {Pierce, Benjamin C.}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
171 title = {Types and Programming Languages}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
172 year = {2002}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
173 isbn = {0262162091, 9780262162098}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
174 edition = {1st}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
175 publisher = {The MIT Press}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
176 } |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
177 |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
178 @book{pierce2013型システム入門プログラミング言語と型の理論, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
179 title={型システム入門プログラミング言語と型の理論: }, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
180 author={Pierce, B.C.}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
181 isbn={9784274069116}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
182 url={https://books.google.co.jp/books?id=Sx8UmwEACAAJ}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
183 year={2013}, |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
184 publisher={オーム社} |
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
185 } |
74 | 186 |
187 @inproceedings{Norell:2009:DTP:1481861.1481862, | |
188 author = {Norell, Ulf}, | |
189 title = {Dependently Typed Programming in Agda}, | |
190 booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation}, | |
191 series = {TLDI '09}, | |
192 year = {2009}, | |
193 isbn = {978-1-60558-420-1}, | |
194 location = {Savannah, GA, USA}, | |
195 pages = {1--2}, | |
196 numpages = {2}, | |
197 url = {http://doi.acm.org/10.1145/1481861.1481862}, | |
198 doi = {10.1145/1481861.1481862}, | |
199 acmid = {1481862}, | |
200 publisher = {ACM}, | |
201 address = {New York, NY, USA}, | |
202 keywords = {dependent types, programming}, | |
203 } | |
204 | |
205 @article{Backus:1978:HFI:960118.808380, | |
206 author = {Backus, John}, | |
207 title = {The History of FORTRAN I, II, and III}, | |
208 journal = {SIGPLAN Not.}, | |
209 issue_date = {August 1978}, | |
210 volume = {13}, | |
211 number = {8}, | |
212 month = aug, | |
213 year = {1978}, | |
214 issn = {0362-1340}, | |
215 pages = {165--180}, | |
216 numpages = {16}, | |
217 url = {http://doi.acm.org/10.1145/960118.808380}, | |
218 doi = {10.1145/960118.808380}, | |
219 acmid = {808380}, | |
220 publisher = {ACM}, | |
221 address = {New York, NY, USA}, | |
222 } | |
223 | |
224 @ARTICLE{Landin64, | |
225 AUTHOR = {Peter J. Landin}, | |
226 TITLE = {The Mechanical Evaluation of Expressions}, | |
227 JOURNAL = {Computer Journal}, | |
228 VOLUME = 6, | |
229 NUMBER = 4, | |
230 MONTH = JAN, | |
231 YEAR = 1964, | |
232 PAGES = {308--320}, | |
233 CHECKED = {5 June 1992, by JCR} | |
234 } | |
235 @book{GlossarWiki:Church:1941, | |
236 author = {Church, Alonzo}, | |
237 title = {The Calculi of Lambda-Conversion}, | |
238 publisher = {Princeton University Press}, | |
239 year = {1941}, | |
240 address = {Princeton, New Jork}, | |
241 url = {http://books.google.de/books/about/The_Calculi_of_Lambda_conversion.html?id=KCOuGztKVgcC}, | |
242 quality = {5}, | |
243 note = {} | |
244 } | |
245 | |
246 @article{haskell-sigplan | |
247 ,author="Hudak, P. and Peyton Jones, S. and Wadler (editors), P." | |
248 ,title="Report on the {P}rogramming {L}anguage {H}askell, | |
249 {A} {N}on-strict {P}urely {F}unctional {L}anguage ({V}ersion 1.2)" | |
250 ,journal="ACM SIGPLAN Notices" | |
251 ,volume=27 | |
252 ,number=5 | |
253 ,month=May | |
254 ,year=1992 | |
255 } | |
256 | |
257 @article{DEBRUIJN1972381, | |
258 title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem", | |
259 journal = "Indagationes Mathematicae (Proceedings)", | |
260 volume = "75", | |
261 number = "5", | |
262 pages = "381 - 392", | |
263 year = "1972", | |
264 note = "", | |
265 issn = "1385-7258", | |
266 doi = "http://dx.doi.org/10.1016/1385-7258(72)90034-0", | |
267 url = "http://www.sciencedirect.com/science/article/pii/1385725872900340", | |
268 author = "N.G de Bruijn", | |
269 | |
270 } |