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