1 @misc{moore1965cramming, |
1 |
2 title={Cramming more components onto integrated circuits}, |
2 @article{moore1965cramming, |
3 author={Moore, Gordon E and others}, |
3 title={{Cramming More Components onto Integrated Circuits}}, |
|
4 author={Moore, Gordon E}, |
4 year={1965}, |
5 year={1965}, |
5 publisher={McGraw-Hill New York, NY, USA} |
6 journal={Electronics}, |
|
7 pages = {114--117}, |
|
8 month = {apr}, |
|
9 day = {19}, |
|
10 number={8}, |
|
11 volume={38} |
6 } |
12 } |
7 |
13 |
8 @article{sutter2005free, |
14 @article{sutter2005free, |
9 title={The free lunch is over: A fundamental turn toward concurrency in software}, |
15 title={The free lunch is over: A fundamental turn toward concurrency in software}, |
10 author={Sutter, Herb}, |
16 author={Sutter, Herb}, |
11 journal={Dr. Dobb’s Journal}, |
17 journal={Dr. Dobb’s Journal}, |
12 volume={30}, |
18 volume={30}, |
13 number={3}, |
19 number={3}, |
14 pages={202--210}, |
20 pages={202--210}, |
15 year={2005} |
21 year={2005}, |
|
22 url = {http://www.gotw.ca/publications/concurrency-ddj.htm} |
16 } |
23 } |
17 |
24 |
18 @article{sutter2005software, |
25 @article{sutter2005software, |
19 title={Software and the concurrency revolution}, |
26 author = {Herb Sutter and |
20 author={Sutter, Herb and Larus, James}, |
27 James R. Larus}, |
21 journal={Queue}, |
28 title = {Software and the concurrency revolution}, |
22 volume={3}, |
29 journal = {ACM Queue}, |
23 number={7}, |
30 volume = {3}, |
24 pages={54--62}, |
31 number = {7}, |
25 year={2005}, |
32 year = {2005}, |
26 publisher={ACM} |
33 pages = {54-62}, |
|
34 ee = {http://doi.acm.org/10.1145/1095408.1095421}, |
|
35 bibsource = {DBLP, http://dblp.uni-trier.de} |
27 } |
36 } |
28 |
37 |
29 @inproceedings{luebke2006gpgpu, |
38 @inproceedings{luebke2006gpgpu, |
30 title={GPGPU: general-purpose computation on graphics hardware}, |
39 author = {Luebke, David and Harris, Mark and Kr\"{u}ger, Jens and Purcell, Tim and Govindaraju, Naga and Buck, Ian and Woolley, Cliff and Lefohn, Aaron}, |
31 author={Luebke, David and Harris, Mark and Govindaraju, Naga and Lefohn, Aaron and Houston, Mike and Owens, John and Segal, Mark and Papakipos, Matthew and Buck, Ian}, |
40 title = {GPGPU: General Purpose Computation on Graphics Hardware}, |
32 booktitle={Proceedings of the 2006 ACM/IEEE conference on Supercomputing}, |
41 booktitle = {ACM SIGGRAPH 2004 Course Notes}, |
33 pages={208}, |
42 series = {SIGGRAPH '04}, |
34 year={2006}, |
43 year = {2004}, |
35 organization={ACM} |
44 venue = {Los Angeles, CA}, |
36 } |
45 articleno = {33}, |
|
46 url = {http://doi.acm.org/10.1145/1103900.1103933}, |
|
47 doi = {10.1145/1103900.1103933}, |
|
48 acmid = {1103933}, |
|
49 publisher = {ACM}, |
|
50 address = {New York, NY, USA}, |
|
51 } |
37 |
52 |
38 @book{burge1975recursive, |
53 @book{burge1975recursive, |
39 title={Recursive programming techniques}, |
54 title={Recursive programming techniques}, |
40 author={Burge, William H}, |
55 author={Burge, William H}, |
41 year={1975}, |
56 year={1975}, |
42 publisher={Addison-Wesley Reading} |
57 publisher={Addison-Wesley Reading} |
43 } |
58 } |
44 |
59 |
45 @book{paulson1994isabelle, |
60 @book{paulson1994isabelle, |
46 title={Isabelle: A generic theorem prover}, |
61 author = {Lawrence C. Paulson}, |
47 author={Paulson, Lawrence C}, |
62 title = {Isabelle - A Generic Theorem Prover}, |
48 volume={828}, |
63 publisher = {Springer-Verlag}, |
49 year={1994}, |
64 series = {Lecture Notes in Computer Science}, |
50 publisher={Springer} |
65 volume = {828}, |
|
66 year = {1994}, |
|
67 isbn = {3-540-58244-4}, |
|
68 ee = {http://dx.doi.org/10.1007/BFb0030541}, |
|
69 bibsource = {DBLP, http://dblp.uni-trier.de} |
51 } |
70 } |
52 |
71 |
53 @phdthesis{neuper2001reactive, |
72 @phdthesis{neuper2001reactive, |
54 title={Reactive user-guidance by an autonomous engine doing high-school math}, |
73 title={Reactive User-Guidance by an Autonomous Engine Doing High-School Math}, |
55 author={Neuper, Walther A}, |
74 author={Neuper, Walther}, |
56 year={2001}, |
75 year={2001}, |
57 school={PhD thesis, IICM-Inst. f. Softwaretechnology, Technical University, A-8010 Graz, 2001. ftp://ftp. ist. tugraz. at/pub/projects/isac/publ/wn-diss. ps. gz} |
76 school={Graz University of Technology} |
58 } |
77 } |
|
78 |
|
79 @book{hammond2000research, |
|
80 editor = {Hammond, Kevin and Michelson, Greg}, |
|
81 title = {Research Directions in Parallel Functional Programming}, |
|
82 year = {2000}, |
|
83 isbn = {1852330929}, |
|
84 publisher = {Springer-Verlag}, |
|
85 address = {London, UK, UK}, |
|
86 } |
|
87 |
|
88 @article{hudak1989conception, |
|
89 author = {Hudak, Paul}, |
|
90 title = {Conception, Evolution, and Application of Functional Programming Languages}, |
|
91 journal = {ACM Comput. Surv.}, |
|
92 issue_date = {Sep. 1989}, |
|
93 volume = {21}, |
|
94 number = {3}, |
|
95 month = sep, |
|
96 year = {1989}, |
|
97 issn = {0360-0300}, |
|
98 pages = {359--411}, |
|
99 numpages = {53}, |
|
100 url = {http://doi.acm.org/10.1145/72551.72554}, |
|
101 doi = {10.1145/72551.72554}, |
|
102 acmid = {72554}, |
|
103 publisher = {ACM}, |
|
104 address = {New York, NY, USA}, |
|
105 } |
|
106 |
|
107 @article{church1932set, |
|
108 title={A set of postulates for the foundation of logic}, |
|
109 author={Church, Alonzo}, |
|
110 journal={Annals of mathematics}, |
|
111 volume={33}, |
|
112 number={2}, |
|
113 pages={346--366}, |
|
114 year={1932} |
|
115 } |
|
116 |
|
117 @article{church1940formulation, |
|
118 author = {Alonzo Church}, |
|
119 title = {A Formulation of the Simple Theory of Types}, |
|
120 journal = {Journal of Symbolic Logic}, |
|
121 volume = {5}, |
|
122 number = {2}, |
|
123 year = {1940}, |
|
124 pages = {56-68}, |
|
125 ee = {http://projecteuclid.org/euclid.jsl/1183387805}, |
|
126 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
127 } |
|
128 |
|
129 @article{mccarthy1978history, |
|
130 author = {McCarthy, John}, |
|
131 title = {History of LISP}, |
|
132 journal = {SIGPLAN Not.}, |
|
133 issue_date = {August 1978}, |
|
134 volume = {13}, |
|
135 number = {8}, |
|
136 month = aug, |
|
137 year = {1978}, |
|
138 issn = {0362-1340}, |
|
139 pages = {217--223}, |
|
140 numpages = {7}, |
|
141 url = {http://doi.acm.org/10.1145/960118.808387}, |
|
142 doi = {10.1145/960118.808387}, |
|
143 acmid = {808387}, |
|
144 publisher = {ACM}, |
|
145 address = {New York, NY, USA}, |
|
146 } |
|
147 |
|
148 @article{backus1978can, |
|
149 author = {John W. Backus}, |
|
150 title = {Can Programming Be Liberated From the von Neumann Style? |
|
151 A Functional Style and its Algebra of Programs}, |
|
152 journal = {Communications of the ACM}, |
|
153 volume = {21}, |
|
154 number = {8}, |
|
155 year = {1978}, |
|
156 pages = {613-641}, |
|
157 ee = {http://doi.acm.org/10.1145/359576.359579}, |
|
158 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
159 } |
|
160 |
|
161 @article{milner1978theory, |
|
162 author = {Robin Milner}, |
|
163 title = {A Theory of Type Polymorphism in Programming}, |
|
164 journal = {Journal of Computer and System Sciences}, |
|
165 volume = {17}, |
|
166 number = {3}, |
|
167 year = {1978}, |
|
168 pages = {348-375}, |
|
169 ee = {http://dx.doi.org/10.1016/0022-0000(78)90014-4}, |
|
170 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
171 } |
|
172 |
|
173 @book{milner1997definition, |
|
174 author = {Milner, Robin and Tofte, Mads and Macqueen, David}, |
|
175 title = {The Definition of Standard ML}, |
|
176 year = {1997}, |
|
177 isbn = {0262631814}, |
|
178 publisher = {MIT Press}, |
|
179 address = {Cambridge, MA, USA}, |
|
180 } |
|
181 |
|
182 @article{jones2003haskell, |
|
183 author = {Simon {Peyton Jones} and others}, |
|
184 title = {The {Haskell} 98 Language and Libraries: The Revised Report}, |
|
185 journal = {Journal of Functional Programming}, |
|
186 volume = 13, |
|
187 number = 1, |
|
188 pages = {0--255}, |
|
189 month = {Jan}, |
|
190 year = 2003, |
|
191 url = {http://www.haskell.org/definition/}, |
|
192 } |
|
193 |
|
194 @online{haskell2013functional, |
|
195 title={Functional programming - HaskellWiki}, |
|
196 url={http://www.haskell.org/haskellwiki/Functional_programming}, |
|
197 year={2013} |
|
198 } |
|
199 |
|
200 @inproceedings{peyton1993imperative, |
|
201 author = {Simon L. Peyton Jones and |
|
202 Philip Wadler}, |
|
203 title = {Imperative Functional Programming}, |
|
204 booktitle = {POPL}, |
|
205 year = {1993}, |
|
206 pages = {71-84}, |
|
207 ee = {http://doi.acm.org/10.1145/158511.158524}, |
|
208 crossref = {DBLP:conf/popl/1993}, |
|
209 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
210 } |
|
211 |
|
212 @article{achten1995ins, |
|
213 author = {Peter Achten and |
|
214 Marinus J. Plasmeijer}, |
|
215 title = {The Ins and Outs of Clean I/O}, |
|
216 journal = {Journal of Functional Programming}, |
|
217 volume = {5}, |
|
218 number = {1}, |
|
219 year = {1995}, |
|
220 pages = {81-110}, |
|
221 ee = {http://dx.doi.org/10.1017/S0956796800001258}, |
|
222 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
223 } |
|
224 |
|
225 @inproceedings{wadler1990linear, |
|
226 AUTHOR = {P. Wadler}, |
|
227 TITLE = {Linear types can change the world!}, |
|
228 BOOKTITLE = {{IFIP {TC} 2} Working Conference on Programming Concepts and Methods}, |
|
229 WHERE = {{Sea of Galilee, Israel}}, |
|
230 PUBLISHER = {North Holland}, |
|
231 EDITOR = {M. Broy and C. Jones}, |
|
232 PAGES = {347--359}, |
|
233 YEAR = {1990} |
|
234 } |
|
235 |
|
236 @inproceedings{launchbury1993natural, |
|
237 author = {Launchbury, John}, |
|
238 title = {A Natural Semantics for Lazy Evaluation}, |
|
239 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, |
|
240 series = {POPL '93}, |
|
241 year = {1993}, |
|
242 isbn = {0-89791-560-7}, |
|
243 venue = {Charleston, South Carolina, USA}, |
|
244 pages = {144--154}, |
|
245 numpages = {11}, |
|
246 url = {http://doi.acm.org/10.1145/158511.158618}, |
|
247 doi = {10.1145/158511.158618}, |
|
248 acmid = {158618}, |
|
249 publisher = {ACM}, |
|
250 address = {New York, NY, USA}, |
|
251 } |
|
252 |
|
253 @phdthesis{lippmeier2009type, |
|
254 title={Type Inference and Optimisation for an Impure World}, |
|
255 author={Lippmeier, Ben}, |
|
256 year={2009}, |
|
257 school={Australian National University} |
|
258 } |
|
259 |
|
260 @inproceedings{amdahl1967validity, |
|
261 author = {Amdahl, Gene M.}, |
|
262 title = {Validity of the Single Processor Approach to Achieving Large Scale Computing Capabilities}, |
|
263 booktitle = {Proceedings of the April 18-20, 1967, Spring Joint Computer Conference}, |
|
264 series = {AFIPS '67 (Spring)}, |
|
265 year = {1967}, |
|
266 venue = {Atlantic City, New Jersey}, |
|
267 pages = {483--485}, |
|
268 numpages = {3}, |
|
269 url = {http://doi.acm.org/10.1145/1465482.1465560}, |
|
270 doi = {10.1145/1465482.1465560}, |
|
271 acmid = {1465560}, |
|
272 publisher = {ACM}, |
|
273 address = {New York, NY, USA}, |
|
274 } |
|
275 |
|
276 @article{gustafson1988reevaluating, |
|
277 author = {John L. Gustafson}, |
|
278 title = {Reevaluating Amdahl's Law}, |
|
279 journal = {Communications of the ACM}, |
|
280 volume = {31}, |
|
281 number = {5}, |
|
282 year = {1988}, |
|
283 pages = {532-533}, |
|
284 ee = {http://doi.acm.org/10.1145/42411.42415}, |
|
285 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
286 } |
|
287 |
|
288 @article{moler1986matrix, |
|
289 title={Matrix computation on distributed memory multiprocessors}, |
|
290 author={Moler, Cleve}, |
|
291 journal={Hypercube Multiprocessors}, |
|
292 volume={86}, |
|
293 pages={181--195}, |
|
294 year={1986} |
|
295 } |
|
296 |
|
297 @article{geer2005chip, |
|
298 author = {David Geer}, |
|
299 title = {Industry Trends: Chip Makers Turn to Multicore Processors}, |
|
300 journal = {IEEE Computer}, |
|
301 volume = {38}, |
|
302 number = {5}, |
|
303 year = {2005}, |
|
304 pages = {11-13}, |
|
305 ee = {http://doi.ieeecomputersociety.org/10.1109/MC.2005.160}, |
|
306 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
307 } |
|
308 |
|
309 @book{culler1999parallel, |
|
310 author = {David E. Culler and |
|
311 Jaswinder Pal Singh and |
|
312 Anoop Gupta}, |
|
313 title = {Parallel computer architecture - a hardware / software approach}, |
|
314 publisher = {Morgan Kaufmann}, |
|
315 year = {1999}, |
|
316 isbn = {978-1-55860-343-1}, |
|
317 pages = {I-XXIX, 1-1024}, |
|
318 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
319 } |
|
320 |
|
321 @book{hennessy2012computer, |
|
322 author = {John L. Hennessy and |
|
323 David A. Patterson}, |
|
324 title = {Computer Architecture - A Quantitative Approach (5. ed.)}, |
|
325 publisher = {Morgan Kaufmann}, |
|
326 year = {2012}, |
|
327 isbn = {978-0-12-383872-8}, |
|
328 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
329 } |
|
330 |
|
331 @inproceedings{tullsen1995simultaneous, |
|
332 author = {Tullsen, Dean M. and Eggers, Susan J. and Levy, Henry M.}, |
|
333 title = {Simultaneous Multithreading: Maximizing On-chip Parallelism}, |
|
334 booktitle = {Proceedings of the 22nd Annual International Symposium on Computer Architecture}, |
|
335 series = {ISCA '95}, |
|
336 year = {1995}, |
|
337 isbn = {0-89791-698-0}, |
|
338 venue = {S. Margherita Ligure, Italy}, |
|
339 pages = {392--403}, |
|
340 numpages = {12}, |
|
341 url = {http://doi.acm.org/10.1145/223982.224449}, |
|
342 doi = {10.1145/223982.224449}, |
|
343 acmid = {224449}, |
|
344 publisher = {ACM}, |
|
345 address = {New York, NY, USA}, |
|
346 } |
|
347 |
|
348 @article{moore2008multicore, |
|
349 title={Multicore is bad news for supercomputers}, |
|
350 author={Moore, Samuel K}, |
|
351 journal={Spectrum, IEEE}, |
|
352 volume={45}, |
|
353 number={11}, |
|
354 pages={15}, |
|
355 year={2008}, |
|
356 publisher={IEEE}, |
|
357 month={nov} |
|
358 } |
|
359 |
|
360 @inproceedings{li2007efficient, |
|
361 author = {Li, Tong and Baumberger, Dan and Koufaty, David A. and Hahn, Scott}, |
|
362 title = {Efficient Operating System Scheduling for Performance-Asymmetric Multi-Core Architectures}, |
|
363 booktitle = {Proceedings of the 2007 ACM/IEEE Conference on Supercomputing}, |
|
364 series = {SC '07}, |
|
365 year = {2007}, |
|
366 isbn = {978-1-59593-764-3}, |
|
367 venue = {Reno, Nevada}, |
|
368 pages = {53:1--53:11}, |
|
369 articleno = {53}, |
|
370 numpages = {11}, |
|
371 url = {http://doi.acm.org/10.1145/1362622.1362694}, |
|
372 doi = {10.1145/1362622.1362694}, |
|
373 acmid = {1362694}, |
|
374 publisher = {ACM}, |
|
375 address = {New York, NY, USA}, |
|
376 } |
|
377 |
|
378 @article{henderson1986functional, |
|
379 author = {Peter B. Henderson}, |
|
380 title = {Functional Programming, Formal Specification, and Rapid |
|
381 Prototyping}, |
|
382 journal = {IEEE Transactions on Software Engineering}, |
|
383 volume = {12}, |
|
384 number = {2}, |
|
385 year = {1986}, |
|
386 pages = {241-250}, |
|
387 ee = {http://doi.ieeecomputersociety.org/10.1109/TSE.1986.6312939}, |
|
388 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
389 } |
|
390 |
|
391 @inproceedings{harris2007feedback, |
|
392 author = {Harris, Tim and Singh, Satnam}, |
|
393 title = {Feedback Directed Implicit Parallelism}, |
|
394 booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming}, |
|
395 series = {ICFP '07}, |
|
396 year = {2007}, |
|
397 isbn = {978-1-59593-815-2}, |
|
398 venue = {Freiburg, Germany}, |
|
399 pages = {251--264}, |
|
400 numpages = {14}, |
|
401 url = {http://doi.acm.org/10.1145/1291151.1291192}, |
|
402 doi = {10.1145/1291151.1291192}, |
|
403 acmid = {1291192}, |
|
404 publisher = {ACM}, |
|
405 address = {New York, NY, USA}, |
|
406 keywords = {functional programming, haskell, implicit parallelism}, |
|
407 } |
|
408 |
|
409 @article{cantrill2008real, |
|
410 author = {Bryan Cantrill and |
|
411 Jeff Bonwick}, |
|
412 title = {Real-World Concurrency}, |
|
413 journal = {ACM Queue}, |
|
414 volume = {6}, |
|
415 number = {5}, |
|
416 year = {2008}, |
|
417 pages = {16-25}, |
|
418 ee = {http://doi.acm.org/10.1145/1454456.1454462}, |
|
419 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
420 } |
|
421 |
|
422 @inproceedings{thompson2005refactoring, |
|
423 author = {Thompson, Simon}, |
|
424 title = {Refactoring Functional Programs}, |
|
425 booktitle = {Proceedings of the 5th International Conference on Advanced Functional Programming}, |
|
426 series = {AFP'04}, |
|
427 year = {2005}, |
|
428 isbn = {3-540-28540-7, 978-3-540-28540-3}, |
|
429 venue = {Tartu, Estonia}, |
|
430 pages = {331--357}, |
|
431 numpages = {27}, |
|
432 url = {http://dx.doi.org/10.1007/11546382_9}, |
|
433 doi = {10.1007/11546382_9}, |
|
434 acmid = {2162147}, |
|
435 publisher = {Springer-Verlag}, |
|
436 address = {Berlin, Heidelberg}, |
|
437 } |
|
438 |
|
439 @inproceedings{hammer2007proposal, |
|
440 author = {Hammer, Matthew and Acar, Umut A. and Rajagopalan, Mohan and Ghuloum, Anwar}, |
|
441 title = {A Proposal for Parallel Self-adjusting Computation}, |
|
442 booktitle = {Proceedings of the 2007 Workshop on Declarative Aspects of Multicore Programming}, |
|
443 series = {DAMP '07}, |
|
444 year = {2007}, |
|
445 isbn = {978-1-59593-690-5}, |
|
446 venue = {Nice, France}, |
|
447 pages = {3--9}, |
|
448 numpages = {7}, |
|
449 url = {http://doi.acm.org/10.1145/1248648.1248651}, |
|
450 doi = {10.1145/1248648.1248651}, |
|
451 acmid = {1248651}, |
|
452 publisher = {ACM}, |
|
453 address = {New York, NY, USA}, |
|
454 keywords = {change propagation, dynamic dependency graphs, fork-join programs, parallel change propagation, parallelism, self-adjusting computation, series-parallel programs}, |
|
455 } |
|
456 |
|
457 @inproceedings{nocker1991concurrent, |
|
458 author = {N\"{o}cker, E. G. J. M. H. and Smesters, J. E. W. and van Eekelen, M. C. J. D. and Plasmeijer, M. J.}, |
|
459 title = {Concurrent Clean}, |
|
460 booktitle = {Proceedings on Parallel Architectures and Languages Europe: Volume II: Parallel Languages}, |
|
461 series = {PARLE '91}, |
|
462 year = {1991}, |
|
463 isbn = {0-387-54152-7}, |
|
464 venue = {Eindhoven, The Netherlands}, |
|
465 pages = {202--219}, |
|
466 numpages = {18}, |
|
467 url = {http://dl.acm.org/citation.cfm?id=111634.111646}, |
|
468 acmid = {111646}, |
|
469 publisher = {Springer-Verlag New York, Inc.}, |
|
470 address = {New York, NY, USA}, |
|
471 } |
|
472 |
|
473 @inproceedings{marlow2009runtime, |
|
474 author = {Marlow, Simon and Peyton Jones, Simon and Singh, Satnam}, |
|
475 title = {Runtime Support for Multicore Haskell}, |
|
476 booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming}, |
|
477 series = {ICFP '09}, |
|
478 year = {2009}, |
|
479 isbn = {978-1-60558-332-7}, |
|
480 venue = {Edinburgh, Scotland}, |
|
481 pages = {65--78}, |
|
482 numpages = {14}, |
|
483 url = {http://doi.acm.org/10.1145/1596550.1596563}, |
|
484 doi = {10.1145/1596550.1596563}, |
|
485 acmid = {1596563}, |
|
486 publisher = {ACM}, |
|
487 address = {New York, NY, USA}, |
|
488 keywords = {Haskell parallel runtime}, |
|
489 } |
|
490 |
|
491 @article{nickolls2010gpu, |
|
492 author = {John Nickolls and |
|
493 William J. Dally}, |
|
494 title = {The GPU Computing Era}, |
|
495 journal = {IEEE Micro}, |
|
496 volume = {30}, |
|
497 number = {2}, |
|
498 year = {2010}, |
|
499 pages = {56-69}, |
|
500 ee = {http://doi.ieeecomputersociety.org/10.1109/MM.2010.41}, |
|
501 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
502 } |
|
503 |
|
504 @article{tarditi2006accelerator, |
|
505 author = {Tarditi, David and Puri, Sidd and Oglesby, Jose}, |
|
506 title = {Accelerator: Using Data Parallelism to Program GPUs for General-purpose Uses}, |
|
507 journal = {SIGOPS Oper. Syst. Rev.}, |
|
508 issue_date = {December 2006}, |
|
509 volume = {40}, |
|
510 number = {5}, |
|
511 month = {oct}, |
|
512 year = {2006}, |
|
513 issn = {0163-5980}, |
|
514 pages = {325--335}, |
|
515 numpages = {11}, |
|
516 doi = {10.1145/1168917.1168898}, |
|
517 publisher = {ACM}, |
|
518 } |
|
519 |
|
520 @article{blelloch90compiling, |
|
521 author = {Guy E. Blelloch and |
|
522 Gary Sabot}, |
|
523 title = {Compiling Collection-Oriented Languages onto Massively Parallel |
|
524 Computers}, |
|
525 journal = {Journal of Parallel and Distributed Computing}, |
|
526 volume = {8}, |
|
527 number = {2}, |
|
528 year = {1990}, |
|
529 pages = {119--134}, |
|
530 ee = {http://dx.doi.org/10.1016/0743-7315(90)90087-6}, |
|
531 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
532 } |
|
533 |
|
534 @inproceedings{peytonjones2008harnessing, |
|
535 author = {Peyton Jones, Simon}, |
|
536 title = {Harnessing the Multicores: Nested Data Parallelism in Haskell}, |
|
537 booktitle = {Proceedings of the 6th Asian Symposium on Programming Languages and Systems}, |
|
538 series = {APLAS '08}, |
|
539 year = {2008}, |
|
540 isbn = {978-3-540-89329-5}, |
|
541 venue = {Bangalore, India}, |
|
542 pages = {138--138}, |
|
543 numpages = {1}, |
|
544 url = {http://dx.doi.org/10.1007/978-3-540-89330-1_10}, |
|
545 doi = {10.1007/978-3-540-89330-1_10}, |
|
546 acmid = {1485356}, |
|
547 publisher = {Springer-Verlag}, |
|
548 address = {Berlin, Heidelberg}, |
|
549 } |
|
550 |
|
551 @inproceedings{baker1977incremental, |
|
552 author = {Baker,Jr., Henry C. and Hewitt, Carl}, |
|
553 title = {The Incremental Garbage Collection of Processes}, |
|
554 booktitle = {Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages}, |
|
555 year = {1977}, |
|
556 pages = {55--59}, |
|
557 numpages = {5}, |
|
558 url = {http://doi.acm.org/10.1145/800228.806932}, |
|
559 doi = {10.1145/800228.806932}, |
|
560 acmid = {806932}, |
|
561 publisher = {ACM}, |
|
562 address = {New York, NY, USA}, |
|
563 keywords = {Eager evaluation, Garbage collection, Lazy evaluation, Multiprocessing systems, Processor scheduling}, |
|
564 } |
|
565 |
|
566 @article{halstead1985multilisp, |
|
567 author = {Robert H. Halstead Jr.}, |
|
568 title = {Multilisp: A Language for Concurrent Symbolic Computation}, |
|
569 journal = {ACM Transactions on Programming Languages and Systems}, |
|
570 volume = {7}, |
|
571 number = {4}, |
|
572 year = {1985}, |
|
573 pages = {501-538}, |
|
574 ee = {http://doi.acm.org/10.1145/4472.4478}, |
|
575 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
576 } |
|
577 |
|
578 @inproceedings{matthews2010efficient, |
|
579 author = {Matthews, David C.J. and Wenzel, Makarius}, |
|
580 title = {Efficient Parallel Programming in Poly/ML and Isabelle/ML}, |
|
581 booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming}, |
|
582 series = {DAMP '10}, |
|
583 year = {2010}, |
|
584 isbn = {978-1-60558-859-9}, |
|
585 venue = {Madrid, Spain}, |
|
586 pages = {53--62}, |
|
587 numpages = {10}, |
|
588 url = {http://doi.acm.org/10.1145/1708046.1708058}, |
|
589 doi = {10.1145/1708046.1708058}, |
|
590 acmid = {1708058}, |
|
591 publisher = {ACM}, |
|
592 address = {New York, NY, USA}, |
|
593 keywords = {data parallelism, isabelle, parallel standard ml, poly/ml, theorem proving applications}, |
|
594 } |
|
595 |
|
596 @article{wegner1990concepts, |
|
597 author = {Peter Wegner}, |
|
598 title = {Concepts and paradigms of object-oriented programming}, |
|
599 journal = {OOPS Messenger}, |
|
600 volume = {1}, |
|
601 number = {1}, |
|
602 year = {1990}, |
|
603 pages = {7-87}, |
|
604 ee = {http://doi.acm.org/10.1145/382192.383004}, |
|
605 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
606 } |
|
607 |
|
608 @article{shavit1997software, |
|
609 title={Software transactional memory}, |
|
610 author={Shavit, Nir and Touitou, Dan}, |
|
611 journal={Distributed Computing}, |
|
612 volume={10}, |
|
613 number={2}, |
|
614 pages={99--116}, |
|
615 year={1997}, |
|
616 publisher={Springer-Verlag} |
|
617 } |
|
618 |
|
619 @article{herlihy1990linearizability, |
|
620 author = {Herlihy, Maurice P. and Wing, Jeannette M.}, |
|
621 title = {Linearizability: A Correctness Condition for Concurrent Objects}, |
|
622 journal = {ACM Trans. Program. Lang. Syst.}, |
|
623 issue_date = {July 1990}, |
|
624 volume = {12}, |
|
625 number = {3}, |
|
626 month = jul, |
|
627 year = {1990}, |
|
628 issn = {0164-0925}, |
|
629 pages = {463--492}, |
|
630 numpages = {30}, |
|
631 url = {http://doi.acm.org/10.1145/78969.78972}, |
|
632 doi = {10.1145/78969.78972}, |
|
633 acmid = {78972}, |
|
634 publisher = {ACM}, |
|
635 address = {New York, NY, USA}, |
|
636 } |
|
637 |
|
638 @inproceedings{ramadan2009committing, |
|
639 author = {Ramadan, Hany E. and Roy, Indrajit and Herlihy, Maurice and Witchel, Emmett}, |
|
640 title = {Committing Conflicting Transactions in an STM}, |
|
641 booktitle = {Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming}, |
|
642 series = {PPoPP '09}, |
|
643 year = {2009}, |
|
644 isbn = {978-1-60558-397-6}, |
|
645 venue = {Raleigh, NC, USA}, |
|
646 pages = {163--172}, |
|
647 numpages = {10}, |
|
648 url = {http://doi.acm.org/10.1145/1504176.1504201}, |
|
649 doi = {10.1145/1504176.1504201}, |
|
650 acmid = {1504201}, |
|
651 publisher = {ACM}, |
|
652 address = {New York, NY, USA}, |
|
653 keywords = {concurrency control, dependence-aware, serializability, transactional memory}, |
|
654 } |
|
655 |
|
656 @inproceedings{herlihy2003software, |
|
657 author = {Herlihy, Maurice and Luchangco, Victor and Moir, Mark and Scherer,III, William N.}, |
|
658 title = {Software Transactional Memory for Dynamic-sized Data Structures}, |
|
659 booktitle = {Proceedings of the Twenty-second Annual Symposium on Principles of Distributed Computing}, |
|
660 series = {PODC '03}, |
|
661 year = {2003}, |
|
662 isbn = {1-58113-708-7}, |
|
663 venue = {Boston, Massachusetts}, |
|
664 pages = {92--101}, |
|
665 numpages = {10}, |
|
666 url = {http://doi.acm.org/10.1145/872035.872048}, |
|
667 doi = {10.1145/872035.872048}, |
|
668 acmid = {872048}, |
|
669 publisher = {ACM}, |
|
670 address = {New York, NY, USA}, |
|
671 } |
|
672 |
|
673 @patent{zhang2010software, |
|
674 title={Software Transaction Commit Order and Conflict Management}, |
|
675 author={Zhang, L. and Grover, V.K. and Magruder, M.M. and Detlefs, D. and Duffy, J.J. and Graefe, G.}, |
|
676 url={http://www.google.co.in/patents/US7711678}, |
|
677 year={2010}, |
|
678 month={5}, |
|
679 number={US 7711678} |
|
680 } |
|
681 |
|
682 @techreport{ennals2006software, |
|
683 title={Software transactional memory should not be obstruction-free}, |
|
684 author={Ennals, Robert}, |
|
685 year={2006}, |
|
686 institution={Technical Report IRC-TR-06-052, Intel Research Cambridge Tech Report} |
|
687 } |
|
688 |
|
689 @techreport{ennals2005efficient, |
|
690 author = {Ennals, Robert}, |
|
691 title = {Efficient Software Transactional Memory}, |
|
692 institution = {Intel Research Cambridge Tech Report}, |
|
693 number = {IRC-TR-05-051}, |
|
694 pdf = {http://www.cs.wisc.edu/trans-memory/misc-papers/051_Rob_Ennals.pdf}, |
|
695 year = {2005}, |
|
696 month = {Jan} |
|
697 } |
|
698 |
|
699 @inproceedings{saha2006mcrt, |
|
700 author = {Saha, Bratin and Adl-Tabatabai, Ali-Reza and Hudson, Richard L. and Minh, Chi Cao and Hertzberg, Benjamin}, |
|
701 title = {McRT-STM: A High Performance Software Transactional Memory System for a Multi-Core Runtime}, |
|
702 booktitle = {Proceedings of the Eleventh ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming}, |
|
703 series = {PPoPP '06}, |
|
704 year = {2006}, |
|
705 isbn = {1-59593-189-9}, |
|
706 pages = {187--197}, |
|
707 numpages = {11}, |
|
708 doi = {10.1145/1122971.1123001}, |
|
709 publisher = {ACM} |
|
710 } |
|
711 |
|
712 @inproceedings{harris2005composable, |
|
713 author = {Harris, Tim and Marlow, Simon and Peyton-Jones, Simon and Herlihy, Maurice}, |
|
714 title = {Composable Memory Transactions}, |
|
715 booktitle = {Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming}, |
|
716 series = {PPoPP '05}, |
|
717 year = {2005}, |
|
718 isbn = {1-59593-080-9}, |
|
719 venue = {Chicago, IL, USA}, |
|
720 pages = {48--60}, |
|
721 numpages = {13}, |
|
722 url = {http://doi.acm.org/10.1145/1065944.1065952}, |
|
723 doi = {10.1145/1065944.1065952}, |
|
724 acmid = {1065952}, |
|
725 publisher = {ACM}, |
|
726 address = {New York, NY, USA}, |
|
727 keywords = {locks, non-blocking algorithms, transactions}, |
|
728 } |
|
729 |
|
730 @inproceedings{hewitt1973universal, |
|
731 author = {Hewitt, Carl and Bishop, Peter and Steiger, Richard}, |
|
732 title = {A Universal Modular ACTOR Formalism for Artificial Intelligence}, |
|
733 booktitle = {Proceedings of the 3rd International Joint Conference on Artificial Intelligence}, |
|
734 series = {IJCAI'73}, |
|
735 year = {1973}, |
|
736 venue = {Stanford, USA}, |
|
737 pages = {235--245}, |
|
738 numpages = {11}, |
|
739 url = {http://dl.acm.org/citation.cfm?id=1624775.1624804}, |
|
740 acmid = {1624804}, |
|
741 publisher = {Morgan Kaufmann Publishers Inc.}, |
|
742 address = {San Francisco, CA, USA}, |
|
743 } |
|
744 |
|
745 @article{hewitt1977viewing, |
|
746 author = {Carl Hewitt}, |
|
747 title = {Viewing Control Structures as Patterns of Passing Messages}, |
|
748 journal = {Artificial Intelligence}, |
|
749 volume = {8}, |
|
750 number = {3}, |
|
751 year = {1977}, |
|
752 pages = {323--364}, |
|
753 ee = {http://dx.doi.org/10.1016/0004-3702(77)90033-9}, |
|
754 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
755 } |
|
756 |
|
757 @article{agha1985actors, |
|
758 author = {Gul A. Agha}, |
|
759 title = {ACTORS - a model of concurrent computation in distributed |
|
760 systems}, |
|
761 publisher = {MIT Press}, |
|
762 series = {MIT Press series in artificial intelligence}, |
|
763 year = {1990}, |
|
764 isbn = {978-0-262-01092-4}, |
|
765 pages = {I-IX, 1-144}, |
|
766 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
767 } |
|
768 |
|
769 @article{agha1997foundation, |
|
770 author = {Gul Agha and |
|
771 Ian A. Mason and |
|
772 Scott F. Smith and |
|
773 Carolyn L. Talcott}, |
|
774 title = {A Foundation for Actor Computation}, |
|
775 journal = {Journal of Functional Programming}, |
|
776 volume = {7}, |
|
777 number = {1}, |
|
778 year = {1997}, |
|
779 pages = {1--72}, |
|
780 ee = {http://journals.cambridge.org/action/displayAbstract?aid=44065}, |
|
781 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
782 } |
|
783 |
|
784 @misc{thurauakka, |
|
785 title={Akka framework}, |
|
786 author={Thurau, Martin}, |
|
787 year={2012}, |
|
788 howpublished={Paper for Seminar Software Systems Engineering, Universität zu Lübeck}, |
|
789 url={http://media.itm.uni-luebeck.de/teaching/ws2012/sem-sse/martin-thurau-akka.io.pdf} |
|
790 } |
|
791 |
|
792 @inproceedings{karmani2009actor, |
|
793 author = {Karmani, Rajesh K. and Shali, Amin and Agha, Gul}, |
|
794 title = {Actor Frameworks for the JVM Platform: A Comparative Analysis}, |
|
795 booktitle = {Proceedings of the 7th International Conference on Principles and Practice of Programming in Java}, |
|
796 series = {PPPJ '09}, |
|
797 year = {2009}, |
|
798 isbn = {978-1-60558-598-7}, |
|
799 venue = {Calgary, Alberta, Canada}, |
|
800 pages = {11--20}, |
|
801 numpages = {10}, |
|
802 url = {http://doi.acm.org/10.1145/1596655.1596658}, |
|
803 doi = {10.1145/1596655.1596658}, |
|
804 acmid = {1596658}, |
|
805 publisher = {ACM}, |
|
806 address = {New York, NY, USA}, |
|
807 keywords = {JVM, Java, abstractions, actors, comparison, frameworks, libraries, performance, semantics}, |
|
808 } |
|
809 |
|
810 @article{fuggetta1998understanding, |
|
811 author = {Alfonso Fuggetta and |
|
812 Gian Pietro Picco and |
|
813 Giovanni Vigna}, |
|
814 title = {Understanding Code Mobility}, |
|
815 journal = {IEEE Transactions on Software Engineering}, |
|
816 volume = {24}, |
|
817 number = {5}, |
|
818 year = {1998}, |
|
819 pages = {342-361}, |
|
820 ee = {http://doi.ieeecomputersociety.org/10.1109/32.685258}, |
|
821 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
822 } |
|
823 |
|
824 @article{panwar1994methodology, |
|
825 author = {Rajendra Panwar and |
|
826 Gul Agha}, |
|
827 title = {A Methodology for Programming Scalable Architectures}, |
|
828 journal = {Journal of Parallel and Distributed Computing}, |
|
829 volume = {22}, |
|
830 number = {3}, |
|
831 year = {1994}, |
|
832 pages = {479-487}, |
|
833 ee = {http://dx.doi.org/10.1006/jpdc.1994.1105}, |
|
834 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
835 } |
|
836 |
|
837 @techreport{odersky2004overview, |
|
838 title={An overview of the Scala programming language}, |
|
839 author={Martin Odersky and Vincent Cremet and Iulian Dragos and Gilles Dubochet and Burak Emir and Sean McDirmid and Stéphane Micheloud and Nikolay Mihaylov and Michel Schinz and Erik Stenman and Lex Spoon and Matthias Zenger}, |
|
840 year={2006}, |
|
841 institution={École Polytechnique Fédérale de Lausanne}, |
|
842 address={1015 Lausanne, Switzerland}, |
|
843 number={LAMP-REPORT-2006-001}, |
|
844 note={2nd edition} |
|
845 } |
|
846 |
|
847 @incollection{haller2006event, |
|
848 title={Event-based programming without inversion of control}, |
|
849 author={Haller, Philipp and Odersky, Martin}, |
|
850 booktitle={Modular Programming Languages}, |
|
851 pages={4--22}, |
|
852 year={2006}, |
|
853 publisher={Springer-Verlag} |
|
854 } |
|
855 |
|
856 @article{haller2009scala, |
|
857 title={Scala actors: Unifying thread-based and event-based programming}, |
|
858 author={Haller, Philipp and Odersky, Martin}, |
|
859 journal={Theoretical Computer Science}, |
|
860 volume={410}, |
|
861 number={2}, |
|
862 pages={202--220}, |
|
863 year={2009}, |
|
864 publisher={Elsevier} |
|
865 } |
|
866 |
|
867 @online {akka2014futures, |
|
868 title={Futures (Scala) -- Akka Documentation}, |
|
869 url={http://doc.akka.io/docs/akka/current/scala/futures.html}, |
|
870 urldate={2014-06-05}, |
|
871 year={2014} |
|
872 } |
|
873 |
|
874 @online {scala2014migration, |
|
875 title={The Scala Actors Migration Guide - Scala Documentation}, |
|
876 author={Jovanovic, Vojin and Haller, Philipp}, |
|
877 url={http://docs.scala-lang.org/overviews/core/actors-migration-guide.html}, |
|
878 year={2014} |
|
879 } |
|
880 |
|
881 @inproceedings{tasharofi2013scala, |
|
882 author = {Tasharofi, Samira and Dinges, Peter and Johnson, Ralph E.}, |
|
883 title = {Why Do Scala Developers Mix the Actor Model with Other Concurrency Models?}, |
|
884 booktitle = {Proceedings of the 27th European Conference on Object-Oriented Programming}, |
|
885 series = {ECOOP'13}, |
|
886 year = {2013}, |
|
887 isbn = {978-3-642-39037-1}, |
|
888 venue = {Montpellier, France}, |
|
889 pages = {302--326}, |
|
890 numpages = {25}, |
|
891 url = {http://dx.doi.org/10.1007/978-3-642-39038-8_13}, |
|
892 doi = {10.1007/978-3-642-39038-8_13}, |
|
893 acmid = {2525001}, |
|
894 publisher = {Springer-Verlag}, |
|
895 address = {Berlin, Heidelberg}, |
|
896 } |
|
897 |
|
898 @article{hoare1978communicating, |
|
899 author = {C. A. R. Hoare}, |
|
900 title = {Communicating Sequential Processes}, |
|
901 journal = {Communications of the ACM}, |
|
902 volume = {21}, |
|
903 number = {8}, |
|
904 year = {1978}, |
|
905 pages = {666-677}, |
|
906 ee = {http://doi.acm.org/10.1145/359576.359585}, |
|
907 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
908 } |
|
909 |
|
910 @book{INMOS84occam, |
|
911 author = {{INMOS, Ltd.}}, |
|
912 year = {1984}, |
|
913 address = {Englewood Cliffs}, |
|
914 publisher = {Prentice Hall}, |
|
915 title = {The occam programming manual} |
|
916 } |
|
917 |
|
918 @inproceedings{dorward1997programming, |
|
919 author = {Dorward, Sean and Pike, Rob and Winterbottom, Phil}, |
|
920 title = {Programming in Limbo}, |
|
921 booktitle = {Proceedings of the 42Nd IEEE International Computer Conference}, |
|
922 series = {COMPCON '97}, |
|
923 year = {1997}, |
|
924 isbn = {0-8186-7804-6}, |
|
925 pages = {245--}, |
|
926 url = {http://dl.acm.org/citation.cfm?id=792770.793719}, |
|
927 acmid = {793719}, |
|
928 publisher = {IEEE Computer Society}, |
|
929 address = {Washington, DC, USA}, |
|
930 keywords = {programming languages, modules, graphics}, |
|
931 } |
|
932 |
|
933 @inproceedings{pike2012go, |
|
934 author = {Rob Pike}, |
|
935 title = {Go at Google}, |
|
936 booktitle = {Proceedings of the Conference on Systems, Programming, and Applications: Software |
|
937 for Humanity}, |
|
938 year = {2012}, |
|
939 pages = {5-6}, |
|
940 ee = {http://doi.acm.org/10.1145/2384716.2384720}, |
|
941 bibsource = {DBLP, http://dblp.uni-trier.de}, |
|
942 venue = {Tucson, AZ, USA}, |
|
943 editor = {Gary T. Leavens} |
|
944 } |
|
945 |
|
946 @inproceedings{brown2012paraforming, |
|
947 author = {Brown, Christopher and Loidl, Hans-Wolfgang and Hammond, Kevin}, |
|
948 title = {ParaForming: Forming Parallel Haskell Programs Using Novel Refactoring Techniques}, |
|
949 booktitle = {Proceedings of the 12th International Conference on Trends in Functional Programming}, |
|
950 series = {TFP'11}, |
|
951 year = {2012}, |
|
952 isbn = {978-3-642-32036-1}, |
|
953 venue = {Madrid, Spain}, |
|
954 pages = {82--97}, |
|
955 numpages = {16}, |
|
956 url = {http://dx.doi.org/10.1007/978-3-642-32037-8_6}, |
|
957 doi = {10.1007/978-3-642-32037-8_6}, |
|
958 acmid = {2362972}, |
|
959 publisher = {Springer-Verlag}, |
|
960 address = {Berlin, Heidelberg}, |
|
961 } |
|
962 |
|
963 @article{kennedy1991interactive, |
|
964 author = {Ken Kennedy and |
|
965 Kathryn S. McKinley and |
|
966 Chau-Wen Tseng}, |
|
967 title = {Interactive Parallel Programming using the ParaScope Editor}, |
|
968 journal = {IEEE Transactions on Parallel and Distributed Systems}, |
|
969 volume = {2}, |
|
970 number = {3}, |
|
971 year = {1991}, |
|
972 pages = {329-341}, |
|
973 ee = {http://doi.ieeecomputersociety.org/10.1109/71.86108}, |
|
974 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
975 } |
|
976 |
|
977 @inproceedings{wloka2009refactoring, |
|
978 author = {Wloka, Jan and Sridharan, Manu and Tip, Frank}, |
|
979 title = {Refactoring for Reentrancy}, |
|
980 booktitle = {Proceedings of the the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering}, |
|
981 series = {ESEC/FSE '09}, |
|
982 year = {2009}, |
|
983 isbn = {978-1-60558-001-2}, |
|
984 venue = {Amsterdam, The Netherlands}, |
|
985 pages = {173--182}, |
|
986 numpages = {10}, |
|
987 url = {http://doi.acm.org/10.1145/1595696.1595723}, |
|
988 doi = {10.1145/1595696.1595723}, |
|
989 acmid = {1595723}, |
|
990 publisher = {ACM}, |
|
991 address = {New York, NY, USA}, |
|
992 keywords = {program transformation, reentrant code, refactoring}, |
|
993 } |
|
994 |
|
995 @article{dig2011refactoring, |
|
996 author = {Danny Dig}, |
|
997 title = {A Refactoring Approach to Parallelism}, |
|
998 journal = {IEEE Software}, |
|
999 volume = {28}, |
|
1000 number = {1}, |
|
1001 year = {2011}, |
|
1002 pages = {17-22}, |
|
1003 ee = {http://doi.ieeecomputersociety.org/10.1109/MS.2011.1}, |
|
1004 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
1005 } |
|
1006 |
|
1007 @article{brown2013cost, |
|
1008 author = {Christopher Brown and |
|
1009 Marco Danelutto and |
|
1010 Kevin Hammond and |
|
1011 Peter Kilpatrick and |
|
1012 Archibald Elliott}, |
|
1013 title = {Cost-Directed Refactoring for Parallel Erlang Programs}, |
|
1014 journal = {International Journal of Parallel Programming}, |
|
1015 volume = {42}, |
|
1016 number = {4}, |
|
1017 year = {2014}, |
|
1018 pages = {564-582}, |
|
1019 ee = {http://dx.doi.org/10.1007/s10766-013-0266-5}, |
|
1020 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
1021 } |
|
1022 |
|
1023 @inproceedings{brown2012language, |
|
1024 author = {Brown, Christopher and Hammond, Kevin and Danelutto, Marco and Kilpatrick, Peter}, |
|
1025 title = {A Language-Independent Parallel Refactoring Framework}, |
|
1026 booktitle = {Proceedings of the Fifth Workshop on Refactoring Tools}, |
|
1027 series = {WRT '12}, |
|
1028 year = {2012}, |
|
1029 isbn = {978-1-4503-1500-5}, |
|
1030 venue = {Rapperswil, Switzerland}, |
|
1031 pages = {54--58}, |
|
1032 numpages = {5}, |
|
1033 url = {http://doi.acm.org/10.1145/2328876.2328884}, |
|
1034 doi = {10.1145/2328876.2328884}, |
|
1035 acmid = {2328884}, |
|
1036 publisher = {ACM}, |
|
1037 address = {New York, NY, USA}, |
|
1038 keywords = {C/C++, Erlang, ParaPhrase, concurrency, parallelism, patterns, refactoring, skeletons}, |
|
1039 } |
|
1040 |
|
1041 @incollection{hammond2013paraphrase, |
|
1042 year={2013}, |
|
1043 isbn={978-3-642-35886-9}, |
|
1044 booktitle={Formal Methods for Components and Objects}, |
|
1045 volume={7542}, |
|
1046 series={Lecture Notes in Computer Science}, |
|
1047 editor={Beckert, Bernhard and Damiani, Ferruccio and de Boer, FrankS. and Bonsangue, MarcelloM.}, |
|
1048 doi={10.1007/978-3-642-35887-6_12}, |
|
1049 title={The ParaPhrase Project: Parallel Patterns for Adaptive Heterogeneous Multicore Systems}, |
|
1050 url={http://dx.doi.org/10.1007/978-3-642-35887-6_12}, |
|
1051 publisher={Springer-Verlag}, |
|
1052 address={Berlin, Heidelberg}, |
|
1053 author={Hammond, Kevin and Aldinucci, Marco and Brown, Christopher and Cesarini, Francesco and Danelutto, Marco and González-Vélez, Horacio and Kilpatrick, Peter and Keller, Rainer and Rossbory, Michael and Shainer, Gilad}, |
|
1054 pages={218-236}, |
|
1055 language={English} |
|
1056 } |
|
1057 |
|
1058 @inproceedings{li2006comparative, |
|
1059 author = {Li, Huiqing and Thompson, Simon}, |
|
1060 title = {Comparative Study of Refactoring Haskell and Erlang Programs}, |
|
1061 booktitle = {Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation}, |
|
1062 series = {SCAM '06}, |
|
1063 year = {2006}, |
|
1064 isbn = {0-7695-2353-6}, |
|
1065 pages = {197--206}, |
|
1066 numpages = {10}, |
|
1067 url = {http://dx.doi.org/10.1109/SCAM.2006.8}, |
|
1068 doi = {10.1109/SCAM.2006.8}, |
|
1069 acmid = {1174113}, |
|
1070 publisher = {IEEE Computer Society}, |
|
1071 address = {Washington, DC, USA}, |
|
1072 } |
|
1073 |
|
1074 @article{hindley1969principal, |
|
1075 author = {Hindley, R.}, |
|
1076 doi = {10.2307/1995158}, |
|
1077 issn = {00029947}, |
|
1078 journal = {Transactions of the American Mathematical Society}, |
|
1079 pages = {29--60}, |
|
1080 publisher = {American Mathematical Society}, |
|
1081 title = {{The Principal Type-Scheme of an Object in Combinatory Logic}}, |
|
1082 volume = {146}, |
|
1083 year = {1969} |
|
1084 } |
|
1085 |
|
1086 @inproceedings{milner1975logic, |
|
1087 title={{A Logic for Computable Functions with Reflexive and Polymorphic Types}}, |
|
1088 author={Milner, Robin and Morris, Lockwood and Newey, Malcolm}, |
|
1089 year={1975}, |
|
1090 booktitle = {Proceedings of the Conference on Proving and Improving Programs} |
|
1091 } |
|
1092 |
|
1093 @phdthesis{damas1984type, |
|
1094 title={Type assignment in programming languages.}, |
|
1095 author={Damas, Luis Manuel Martins}, |
|
1096 year={1984}, |
|
1097 school={University of Edinburgh} |
|
1098 } |
|
1099 |
|
1100 @article{paulson1989foundation, |
|
1101 author = {Lawrence C. Paulson}, |
|
1102 title = {The Foundation of a Generic Theorem Prover}, |
|
1103 journal = {Journal of Automated Reasoning}, |
|
1104 volume = {5}, |
|
1105 number = {3}, |
|
1106 year = {1989}, |
|
1107 pages = {363-397}, |
|
1108 ee = {http://dx.doi.org/10.1007/BF00248324}, |
|
1109 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
1110 } |
|
1111 |
|
1112 @inproceedings{weeks2006whole, |
|
1113 author = {Weeks, Stephen}, |
|
1114 title = {Whole-program Compilation in MLton}, |
|
1115 booktitle = {Proceedings of the 2006 Workshop on ML}, |
|
1116 series = {ML '06}, |
|
1117 year = {2006}, |
|
1118 isbn = {1-59593-483-9}, |
|
1119 venue = {Portland, Oregon, USA}, |
|
1120 pages = {1--1}, |
|
1121 numpages = {1}, |
|
1122 url = {http://doi.acm.org/10.1145/1159876.1159877}, |
|
1123 doi = {10.1145/1159876.1159877}, |
|
1124 acmid = {1159877}, |
|
1125 publisher = {ACM}, |
|
1126 address = {New York, NY, USA}, |
|
1127 } |
|
1128 |
|
1129 @online{smlnj2013standard, |
|
1130 url={http://www.smlnj.org/}, |
|
1131 title={Standard ML of New Jersey}, |
|
1132 author={SML/NJ Fellowship, The}, |
|
1133 urldate={2014-05-15} |
|
1134 } |
|
1135 |
|
1136 @online{romanenko2014moscow, |
|
1137 url={http://mosml.org/}, |
|
1138 title={Moscow ML}, |
|
1139 year={2014-05-15} |
|
1140 } |
|
1141 |
|
1142 @online{matthews2014documentation, |
|
1143 url={http://polyml.org/Doc.html}, |
|
1144 title={Documentation}, |
|
1145 author={Matthews, David C.J.}, |
|
1146 year={2014-05-15} |
|
1147 } |
|
1148 |
|
1149 @techreport{matthews1995papers, |
|
1150 author = {Matthews, David CJ}, |
|
1151 title = {{Papers on Poly/ML}}, |
|
1152 year = {1989}, |
|
1153 month = {feb}, |
|
1154 institution = {Computer Laboratory, University of Cambridge} |
|
1155 } |
|
1156 |
|
1157 @techreport{matthews1991distributed, |
|
1158 title={A Distributed Concurrent Implementation of Standard ML}, |
|
1159 author={Matthews, David CJ}, |
|
1160 year={1991}, |
|
1161 institution={LFCS, Department of Computer Science, University of Edinburgh} |
|
1162 } |
|
1163 |
|
1164 @inproceedings{reppy1993concurrent, |
|
1165 author = {Reppy, John H.}, |
|
1166 title = {Concurrent ML: Design, Application and Semantics}, |
|
1167 booktitle = {Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992}, |
|
1168 venue={McMaster University, Hamilton, Ontario, Canada}, |
|
1169 year = {1993}, |
|
1170 isbn = {3-540-56883-2}, |
|
1171 pages = {165--198}, |
|
1172 numpages = {34}, |
|
1173 publisher = {Springer-Verlag} |
|
1174 } |
|
1175 |
|
1176 @manual{wenzel2013isar, |
|
1177 title={The Isabelle/Isar Reference Manual}, |
|
1178 author={Wenzel, Makarius and others}, |
|
1179 year={2013}, |
|
1180 url={http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf} |
|
1181 } |
|
1182 |
|
1183 @incollection{wenzel1999isar, |
|
1184 volume={1690}, |
|
1185 series={Lecture Notes in Computer Science}, |
|
1186 editor={Bertot, Yves and Dowek, Gilles and Théry, Laurent and Hirschowitz, André and Paulin, Christine}, |
|
1187 doi={10.1007/3-540-48256-3_12}, |
|
1188 title={Isar — A Generic Interpretative Approach to Readable Formal Proof Documents}, |
|
1189 author={Wenzel, Makarius}, |
|
1190 booktitle={Theorem Proving in Higher Order Logics}, |
|
1191 pages={167--183}, |
|
1192 year={1999}, |
|
1193 publisher={Springer-Verlag}, |
|
1194 address={Berlin, Heidelberg}, |
|
1195 isbn={978-3-540-66463-5} |
|
1196 } |
|
1197 |
|
1198 @inproceedings{wenzel2014uipide, |
|
1199 title={Asynchronous User Interaction and Tool Integration in Isabelle/PIDE}, |
|
1200 author={Wenzel, Makarius}, |
|
1201 year={2014}, |
|
1202 month = {jul}, |
|
1203 booktitle={Proceedings of the 5th Int.\ Conference on Interactive Theorem Proving}, |
|
1204 venue={Vienna, Austria}, |
|
1205 editor = {Klein, G and Gamboa, R} |
|
1206 } |
|
1207 |
|
1208 @inproceedings{matichuk2014isabelle, |
|
1209 author = {Matichuk, Daniel and Wenzel, Makarius and Murray, Toby}, |
|
1210 month = {jul}, |
|
1211 year = {2014}, |
|
1212 title = {An Isabelle Proof Method Language}, |
|
1213 booktitle={Proceedings of the 5th Int.\ Conference on Interactive Theorem Proving}, |
|
1214 publisher = {Springer-Verlag}, |
|
1215 venue={Vienna, Austria}, |
|
1216 editor = {Klein, G and Gamboa, R} |
|
1217 } |
|
1218 |
|
1219 @article{wenzel2012asynchronous, |
|
1220 author = {Makarius Wenzel}, |
|
1221 title = {Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit}, |
|
1222 journal = {Electronic Notes in Theoretical Computer Science}, |
|
1223 volume = {285}, |
|
1224 year = {2012}, |
|
1225 pages = {101--114} |
|
1226 } |
|
1227 |
|
1228 @manual{wenzel2013isabelle, |
|
1229 title={The Isabelle System Manual}, |
|
1230 author={Wenzel, Makarius and Berghofer, Stefan}, |
|
1231 year={2013}, |
|
1232 url={http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/system.pdf} |
|
1233 } |
|
1234 |
|
1235 @inproceedings{wenzel2011isabelle, |
|
1236 author = {Wenzel, Makarius}, |
|
1237 title = {Isabelle As Document-Oriented Proof Assistant}, |
|
1238 booktitle = {Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics}, |
|
1239 series = {MKM'11}, |
|
1240 year = {2011}, |
|
1241 isbn = {978-3-642-22672-4}, |
|
1242 venue = {Bertinoro, Italy}, |
|
1243 pages = {244--259}, |
|
1244 numpages = {16}, |
|
1245 url = {http://dl.acm.org/citation.cfm?id=2032713.2032732}, |
|
1246 acmid = {2032732}, |
|
1247 publisher = {Springer-Verlag}, |
|
1248 address = {Berlin, Heidelberg}, |
|
1249 } |
|
1250 |
|
1251 @inproceedings{wenzel2012isabelle, |
|
1252 author = {Wenzel, Makarius}, |
|
1253 title = {Isabelle/jEdit: A Prover IDE Within the PIDE Framework}, |
|
1254 booktitle = {Proceedings of the 11th International Conference on Intelligent Computer Mathematics}, |
|
1255 series = {CICM'12}, |
|
1256 year = {2012}, |
|
1257 isbn = {978-3-642-31373-8}, |
|
1258 venue = {Bremen, Germany}, |
|
1259 pages = {468--471}, |
|
1260 numpages = {4}, |
|
1261 url = {http://dx.doi.org/10.1007/978-3-642-31374-5_38}, |
|
1262 doi = {10.1007/978-3-642-31374-5_38}, |
|
1263 acmid = {2352851}, |
|
1264 publisher = {Springer-Verlag}, |
|
1265 address = {Berlin, Heidelberg}, |
|
1266 } |
|
1267 |
|
1268 @manual{wenzel2013jedit, |
|
1269 title={Isabelle/jEdit}, |
|
1270 author={Wenzel, Makarius}, |
|
1271 year={2013}, |
|
1272 url={http://isabelle.in.tum.de/dist/doc/jedit.pdf} |
|
1273 } |
|
1274 |
|
1275 @book{chlipala2011certified, |
|
1276 author = {Chlipala, Adam}, |
|
1277 title = {Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant}, |
|
1278 year = {2013}, |
|
1279 isbn = {0262026651, 9780262026659}, |
|
1280 publisher = {The MIT Press}, |
|
1281 } |
|
1282 |
|
1283 @book{nipkow2002isabelle, |
|
1284 author = {Nipkow, Tobias and Wenzel, Makarius and Paulson, Lawrence C.}, |
|
1285 title = {Isabelle/HOL: A Proof Assistant for Higher-order Logic}, |
|
1286 year = {2013}, |
|
1287 month = {12}, |
|
1288 isbn = {3-540-43376-7}, |
|
1289 publisher = {Springer-Verlag} |
|
1290 } |
|
1291 |
|
1292 @manual{wenzel2013impl, |
|
1293 title={The Isabelle/Isar Implementation}, |
|
1294 author={Wenzel, Makarius}, |
|
1295 year={2013}, |
|
1296 note={With contributions by Florian Haftmann and Larry Paulson}, |
|
1297 url={http://isabelle.in.tum.de/doc/implementation.pdf} |
|
1298 } |
|
1299 |
|
1300 @book{van1979checking, |
|
1301 title = {Checking Landau's ``Grundlagen'' in the Automath system}, |
|
1302 author = {van Benthem Jutting, L. S.}, |
|
1303 publisher = {Mathematisch Centrum}, |
|
1304 address = {Eindhoven}, |
|
1305 year = {1979} |
|
1306 } |
|
1307 |
|
1308 @article{landin1966next, |
|
1309 author = {Peter J. Landin}, |
|
1310 title = {The next 700 programming languages}, |
|
1311 journal = {Communications of the ACM}, |
|
1312 volume = {9}, |
|
1313 number = {3}, |
|
1314 year = {1966}, |
|
1315 pages = {157--166} |
|
1316 } |
|
1317 |
|
1318 @inproceedings{paulson1988isabelle, |
|
1319 author = {Paulson, Lawrence C.}, |
|
1320 title = {Isabelle: The Next Seven Hundred Theorem Provers}, |
|
1321 booktitle = {Proceedings of the 9th International Conference on Automated Deduction}, |
|
1322 year = {1988}, |
|
1323 isbn = {3-540-19343-X}, |
|
1324 pages = {772--773}, |
|
1325 numpages = {2}, |
|
1326 url = {http://dl.acm.org/citation.cfm?id=648228.751990}, |
|
1327 acmid = {751990}, |
|
1328 publisher = {Springer-Verlag}, |
|
1329 address = {London, UK, UK}, |
|
1330 } |
|
1331 |
|
1332 @article{gentzen1964investigations, |
|
1333 title={Investigations into logical deduction}, |
|
1334 author={Gentzen, Gerhard}, |
|
1335 journal={American philosophical quarterly}, |
|
1336 volume={1}, |
|
1337 number={4}, |
|
1338 pages={288--306}, |
|
1339 year={1964}, |
|
1340 publisher={JSTOR} |
|
1341 } |
|
1342 |
|
1343 @article{coquand1988calculus, |
|
1344 author = {Thierry Coquand and |
|
1345 G{\'e}rard P. Huet}, |
|
1346 title = {The Calculus of Constructions}, |
|
1347 journal = {Information and Computation}, |
|
1348 volume = {76}, |
|
1349 number = {2/3}, |
|
1350 year = {1988}, |
|
1351 pages = {95-120}, |
|
1352 ee = {http://dx.doi.org/10.1016/0890-5401(88)90005-3}, |
|
1353 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
1354 } |
|
1355 |
|
1356 @article{fitzgerald2008vdmtools, |
|
1357 author = {John S. Fitzgerald and |
|
1358 Peter Gorm Larsen and |
|
1359 Shin Sahara}, |
|
1360 title = {VDMTools: advances in support for formal modeling in VDM}, |
|
1361 journal = {SIGPLAN Notices}, |
|
1362 volume = {43}, |
|
1363 number = {2}, |
|
1364 year = {2008}, |
|
1365 pages = {3-11}, |
|
1366 ee = {http://doi.acm.org/10.1145/1361213.1361214}, |
|
1367 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
1368 } |
|
1369 |
|
1370 @incollection{fitzgerald2008vienna, |
|
1371 title = {Vienna Development Method}, |
|
1372 author = {Fitzgerald, John S. and Larsen, Peter Gorm and Verhoef, Marcel}, |
|
1373 publisher = {John Wiley \& Sons, Inc.}, |
|
1374 isbn = {9780470050118}, |
|
1375 url = {http://dx.doi.org/10.1002/9780470050118.ecse447}, |
|
1376 doi = {10.1002/9780470050118.ecse447}, |
|
1377 booktitle = {Wiley Encyclopedia of Computer Science and Engineering}, |
|
1378 year = {2007} |
|
1379 } |
|
1380 |
|
1381 @book{bjorner2006software, |
|
1382 title={Software Engineering}, |
|
1383 author={Bj{\o}rner, Dines}, |
|
1384 volume={1,2,3}, |
|
1385 year={2006}, |
|
1386 series={Texts in Theoretical Computer Science}, |
|
1387 publisher={Springer-Verlag} |
|
1388 } |
|
1389 |
|
1390 @article{back2010structured, |
|
1391 author = {Ralph-Johan Back}, |
|
1392 title = {Structured derivations: a unified proof style for teaching mathematics}, |
|
1393 journal = {Formal Aspects of Computing}, |
|
1394 volume = {22}, |
|
1395 number = {5}, |
|
1396 year = {2010}, |
|
1397 pages = {629--661} |
|
1398 } |
|
1399 |
|
1400 @article{wenzel2007generic, |
|
1401 title={Isabelle/Isar -- a generic framework for human-readable proof documents}, |
|
1402 author={Wenzel, Makarius}, |
|
1403 journal={From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec}, |
|
1404 volume={10}, |
|
1405 number={23}, |
|
1406 pages={277--298}, |
|
1407 year={2007} |
|
1408 } |
|
1409 |
|
1410 @inproceedings{neuper2012automated, |
|
1411 author = {Walther Neuper}, |
|
1412 title = {Automated Generation of User Guidance by Combining Computation |
|
1413 and Deduction}, |
|
1414 editor = {Pedro Quaresma and |
|
1415 Ralph-Johan Back}, |
|
1416 booktitle = {Proceedings of the First Workshop on CTP Components for Educational |
|
1417 Software (THedu'11)}, |
|
1418 year = {2011}, |
|
1419 pages = {82--101}, |
|
1420 series = {EPTCS}, |
|
1421 volume = {79}, |
|
1422 venue = {Wroclaw, Poland}, |
|
1423 month = {7} |
|
1424 } |
|
1425 |
|
1426 @article{daroczy2013error, |
|
1427 title={Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems}, |
|
1428 author={Dar{\'o}czy, Gabriella and Neuper, Walther}, |
|
1429 journal={Electronic Journal of Mathematics \& Technology}, |
|
1430 volume={7}, |
|
1431 number={2}, |
|
1432 year={2013} |
|
1433 } |
|
1434 |
|
1435 @mastersthesis{kienleitner2012towards, |
|
1436 title={Towards ``NextStep Userguidance'' in a Mechanized Math Assistant}, |
|
1437 author={Kienleitner, Markus}, |
|
1438 school={Graz University of Technology}, |
|
1439 year={2012}, |
|
1440 type={Bachelor's thesis} |
|
1441 } |
|
1442 |
|
1443 @inproceedings{wenzel2009parallel, |
|
1444 author = {Makarius Wenzel}, |
|
1445 title = {{Parallel Proof Checking in {Isabelle/Isar}}}, |
|
1446 booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)}, |
|
1447 year = {2009}, |
|
1448 editor = {Dos Reis, G and L Th\'ery}, |
|
1449 publisher = {ACM Digital Library} |
|
1450 } |
|
1451 |
|
1452 @techreport{buchberger1984mathematik, |
|
1453 author={Buchberger, Bruno}, |
|
1454 title={Mathematik für Informatiker II (Problemlösestrategien und Algorithmentypen)}, |
|
1455 institution={RISC-Linz}, |
|
1456 type={Lecture notes}, |
|
1457 number={CAMP-Publ.-No. 84-4.0}, |
|
1458 year={1984} |
|
1459 } |
|
1460 |
|
1461 @mastersthesis{lehnfeld2011verbindung, |
|
1462 title={Verbindung von 'Computation' und 'Deduction' im \isac{}-System}, |
|
1463 author={Lehnfeld, Mathias}, |
|
1464 school={Technische Universität Wien}, |
|
1465 year={2011}, |
|
1466 type={Bachelor's project report} |
|
1467 } |
|
1468 |
|
1469 @phdthesis{krauss2009automating, |
|
1470 author = {Alexander Krauss}, |
|
1471 title = {Automating recursive definitions and termination proofs |
|
1472 in higher-order logic}, |
|
1473 year = {2009}, |
|
1474 pages = {1-127}, |
|
1475 school = {Technische Universität München}, |
|
1476 ee = {http://mediatum2.ub.tum.de/doc/681651/document.pdf}, |
|
1477 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
1478 } |
|
1479 |
|
1480 @mastersthesis{rocnik2012interactive, |
|
1481 author={Jan Rocnik}, |
|
1482 title={Interactive Course Material for Signal Processing based on Isabelle/\isac{}}, |
|
1483 type={Bachelor's thesis}, |
|
1484 year={2012}, |
|
1485 url={http://www.ist.tugraz.at/projects/isac/publ/jrocnik_bakk.pdf}, |
|
1486 school={Graz University of Technology} |
|
1487 } |
|
1488 |
|
1489 @inproceedings{haftmann2010code, |
|
1490 author = {Haftmann, Florian and Nipkow, Tobias}, |
|
1491 title = {Code Generation via Higher-order Rewrite Systems}, |
|
1492 booktitle = {Proceedings of the 10th International Conference on Functional and Logic Programming}, |
|
1493 series = {FLOPS'10}, |
|
1494 year = {2010}, |
|
1495 isbn = {3-642-12250-7, 978-3-642-12250-7}, |
|
1496 venue = {Sendai, Japan}, |
|
1497 pages = {103--117}, |
|
1498 numpages = {15}, |
|
1499 url = {http://dx.doi.org/10.1007/978-3-642-12251-4_9}, |
|
1500 doi = {10.1007/978-3-642-12251-4_9}, |
|
1501 acmid = {2175441}, |
|
1502 publisher = {Springer-Verlag}, |
|
1503 address = {Berlin, Heidelberg}, |
|
1504 } |
|
1505 |
|
1506 @book{charniak2014artificial, |
|
1507 author = {Charniak, Eugene and Riesbeck, Christopher K. and McDermott, Drew V. and Meehan, James R.}, |
|
1508 title = {Artificial Intelligence Programming}, |
|
1509 edition = {2}, |
|
1510 isbn = {0898596092}, |
|
1511 year = {1987}, |
|
1512 publisher = {Psychology Press} |
|
1513 } |
|
1514 |
|
1515 @inproceedings{aspinall2000proof, |
|
1516 author = {Aspinall, David}, |
|
1517 title = {Proof General: A Generic Tool for Proof Development}, |
|
1518 booktitle = {Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held As Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000}, |
|
1519 series = {TACAS '00}, |
|
1520 year = {2000}, |
|
1521 isbn = {3-540-67282-6}, |
|
1522 pages = {38--42}, |
|
1523 numpages = {5}, |
|
1524 url = {http://dl.acm.org/citation.cfm?id=646484.691773}, |
|
1525 acmid = {691773}, |
|
1526 publisher = {Springer-Verlag}, |
|
1527 address = {London, UK, UK}, |
|
1528 } |
|
1529 |
|
1530 @book{simon1965shape, |
|
1531 address = {New York}, |
|
1532 author = {Simon, H. A.}, |
|
1533 publisher = {Harper \& Row}, |
|
1534 title = {{The Shape of Automation for Men and Management}}, |
|
1535 year = {1965} |
|
1536 } |
|
1537 |
|
1538 @book{gordon1993introduction, |
|
1539 title={Introduction to HOL: A theorem proving environment for higher-order logic}, |
|
1540 author={Gordon, Michael JC and Melham, Tom F}, |
|
1541 year={1993}, |
|
1542 publisher={Cambridge University Press} |
|
1543 } |
|
1544 |
|
1545 @online{harrison2014hol, |
|
1546 author={Harrison, John}, |
|
1547 title={HOL Light}, |
|
1548 urldate={2014-05-26}, |
|
1549 url={http://www.cl.cam.ac.uk/~jrh13/hol-light/} |
|
1550 } |
|
1551 |
|
1552 @article{appel1977solution, |
|
1553 title={The solution of the four-color-map problem}, |
|
1554 author={Appel, Kenneth and Haken, Wolfgang}, |
|
1555 journal={Scientific American}, |
|
1556 volume={237}, |
|
1557 pages={108--121}, |
|
1558 year={1977} |
|
1559 } |
|
1560 |
|
1561 @incollection{hales2011historical, |
|
1562 year={2011}, |
|
1563 isbn={978-1-4614-1128-4}, |
|
1564 booktitle={The Kepler Conjecture}, |
|
1565 editor={Lagarias, Jeffrey C.}, |
|
1566 doi={10.1007/978-1-4614-1129-1_3}, |
|
1567 title={Historical Overview of the Kepler Conjecture}, |
|
1568 url={http://dx.doi.org/10.1007/978-1-4614-1129-1_3}, |
|
1569 publisher={Springer New York}, |
|
1570 author={Hales, ThomasC.}, |
|
1571 pages={65-82}, |
|
1572 language={English} |
|
1573 } |
|
1574 |
|
1575 @techreport{sharangpani1994statistical, |
|
1576 title={Statistical Analysis of Floating Point Flaw in the Pentium Processor}, |
|
1577 author={Sharangpani, HP and Barton, ML}, |
|
1578 institution={Intel Corporation}, |
|
1579 year={1994} |
|
1580 } |
|
1581 |
|
1582 @online{intel1997intel, |
|
1583 year={1997}, |
|
1584 title={Intel® Pentium® Processor - Invalid Instruction Erratum Overview}, |
|
1585 urldate={2014-05-26}, |
|
1586 url={http://www.intel.com/support/processors/pentium/ppiie/index.htm} |
|
1587 } |
|
1588 |
|
1589 @article{brandt2007theorem, |
|
1590 title={Theorem Proving in Higher Order Logics}, |
|
1591 author={Brandt, Klaus Schneider Jens}, |
|
1592 year={2007}, |
|
1593 publisher={Springer-Verlag} |
|
1594 } |
|
1595 |
|
1596 @online{isabelle2013news, |
|
1597 title={isabelle.in.tum.de/dist/Isabelle2013-2/NEWS}, |
|
1598 url={http://isabelle.in.tum.de/dist/Isabelle2013-2/NEWS}, |
|
1599 urldate={2014-05-27}, |
|
1600 year=2013 |
|
1601 } |
|
1602 |
|
1603 @online{isac2014knowledge, |
|
1604 title={www.ist.tugraz.at/projects/isac/www/kbase/thy/index\_thy.html}, |
|
1605 url={http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html}, |
|
1606 urldate={2014-06-01} |
|
1607 } |
|
1608 |
|
1609 @online{isac2014pbl, |
|
1610 title={www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}, |
|
1611 url={http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html}, |
|
1612 urldate={2014-06-01} |
|
1613 } |
|
1614 |
|
1615 @online{isac2014met, |
|
1616 title={www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html}, |
|
1617 url={http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html}, |
|
1618 urldate={2014-06-01} |
|
1619 } |
|
1620 |
|
1621 @manual{krauss2013defining, |
|
1622 title={Defining recursive functions in Isabelle/HOL}, |
|
1623 author={Krauss, Alexander}, |
|
1624 year={2013}, |
|
1625 url={http://isabelle.in.tum.de/doc/functions.pdf} |
|
1626 } |
|
1627 |
|
1628 @online{google2012flyspeck, |
|
1629 title={FlyspeckFactSheet}, |
|
1630 url={https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet}, |
|
1631 urldate={2014-06-01}, |
|
1632 year={2012} |
|
1633 } |
|
1634 |
|
1635 @online{austriaforum2014zemanek, |
|
1636 title={Zemanek, Heinz | Austria-Forum > Biographien}, |
|
1637 url={http://austria-forum.org/af/Wissenssammlungen/Biographien/Zemanek,_Heinz}, |
|
1638 urldate={2014-06-02} |
|
1639 } |
|
1640 |
|
1641 @article{gonthier2008formal, |
|
1642 title={Formal Proof --- The Four Colour Theorem}, |
|
1643 author={Gonthier, Georges}, |
|
1644 journal={Notices of the AMS}, |
|
1645 volume={55}, |
|
1646 number={11}, |
|
1647 pages={1382--1393}, |
|
1648 year={2008} |
|
1649 } |
|
1650 |
|
1651 @online{pipermail2014clisa, |
|
1652 title={The Cl-isabelle-users Archives}, |
|
1653 url={https://lists.cam.ac.uk/pipermail/cl-isabelle-users/}, |
|
1654 urldate={2014-06-05}, |
|
1655 year={2014} |
|
1656 } |
|
1657 |
|
1658 @online{tum2013team, |
|
1659 title={The Team}, |
|
1660 url={http://www21.in.tum.de/team}, |
|
1661 urldate={2014-06-05}, |
|
1662 year={2013} |
|
1663 } |
|
1664 |
|
1665 @online{tum2014isainst, |
|
1666 title={Installation}, |
|
1667 url={http://isabelle.in.tum.de/installation.html}, |
|
1668 urldate={2014-06-05}, |
|
1669 year={2013} |
|
1670 } |
|
1671 |
|
1672 @online{andriusvelykis2013isaclipse, |
|
1673 title={Isabelle/Eclipse}, |
|
1674 url={http://andriusvelykis.github.io/isabelle-eclipse/}, |
|
1675 urldate={2014-06-05}, |
|
1676 year={2013} |
|
1677 } |
|
1678 |
|
1679 @online{emath2013emath, |
|
1680 title={E-Math}, |
|
1681 url={http://emath.eu/en/}, |
|
1682 urldate={2014-06-05}, |
|
1683 year={2013} |
|
1684 } |
|
1685 |
|
1686 @online{tum2013isadoc, |
|
1687 title={Documentation}, |
|
1688 url={http://isabelle.in.tum.de/documentation.html}, |
|
1689 urldate={2014-06-13}, |
|
1690 year={2013}, |
|
1691 OPTnote={Theory libraries for Isabelle2013-2} |
|
1692 } |
|
1693 |
|
1694 @online{wiki2014proofass, |
|
1695 title={Proof assistant - Wikipedia, the free encyclopedia}, |
|
1696 url={http://en.wikipedia.org/wiki/Proof_assistant}, |
|
1697 urldate={2014-06-13}, |
|
1698 year={2014} |
|
1699 } |
|
1700 |
|
1701 @online{wiki2014atp, |
|
1702 title={Automated theorem proving - Wikipedia, the free encyclopedia}, |
|
1703 url={http://en.wikipedia.org/wiki/Automated_theorem_proving}, |
|
1704 urldate={2014-06-13}, |
|
1705 year={2014} |
|
1706 } |
|
1707 |
|
1708 @online{tum2013isahol, |
|
1709 title={Isabelle/HOL sessions}, |
|
1710 url={http://isabelle.in.tum.de/dist/library/HOL/}, |
|
1711 urldate={2014-06-13} |
|
1712 } |
|
1713 |
|
1714 @online{isac2014pblequuniv, |
|
1715 title={www.ist.tugraz.at/projects/isac/www/kbase/pbl/pbl\_equ\_univ.html}, |
|
1716 url={http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/pbl_equ_univ.html}, |
|
1717 urldate={2014-06-13} |
|
1718 } |
|
1719 |
|
1720 @mastersthesis{haller2006object, |
|
1721 title={An Object-Oriented Programming Model for Event-Based Actors}, |
|
1722 author={Haller, Philipp}, |
|
1723 year={2006}, |
|
1724 school={University of Karlsruhe} |
|
1725 } |
|
1726 |
|
1727 @online{wenzel2014actors, |
|
1728 title={Re: [isabelle-dev] scala-2.11.0}, |
|
1729 url={http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg05253.html}, |
|
1730 author={Wenzel, Makarius}, |
|
1731 year={2014}, |
|
1732 urldate={2014-06-16} |
|
1733 } |
|
1734 |
|
1735 @inproceedings{blanchette2011automatic, |
|
1736 author = {Blanchette, Jasmin Christian and Bulwahn, Lukas and Nipkow, Tobias}, |
|
1737 title = {Automatic Proof and Disproof in Isabelle/HOL}, |
|
1738 booktitle = {Proceedings of the 8th International Conference on Frontiers of Combining Systems}, |
|
1739 series = {FroCoS'11}, |
|
1740 year = {2011}, |
|
1741 isbn = {978-3-642-24363-9}, |
|
1742 venue = {Saarbrücken, Germany}, |
|
1743 pages = {12--27}, |
|
1744 numpages = {16}, |
|
1745 url = {http://dl.acm.org/citation.cfm?id=2050784.2050787}, |
|
1746 acmid = {2050787}, |
|
1747 publisher = {Springer-Verlag}, |
|
1748 address = {Berlin, Heidelberg}, |
|
1749 } |
|
1750 |
|
1751 %@inproceedings{wenzel2007sml, |
|
1752 % title={SML with antiquotations embedded into Isabelle/Isar}, |
|
1753 % author={Wenzel, Makarius and Chaieb, Amine}, |
|
1754 % booktitle={Workshop on Programming Languages for Mechanized Mathematics (satellite of CALCULEMUS 2007). %Hagenberg, Austria}, |
|
1755 % year={2007} |
|
1756 %} |
|
1757 |
|
1758 @online{tum2014repo, |
|
1759 title={isabelle: Summary}, |
|
1760 url={http://isabelle.in.tum.de/repos/isabelle/}, |
|
1761 year={2014}, |
|
1762 urldate={2014-06-21} |
|
1763 } |