2 @article{moore1965cramming,
3 title={{Cramming More Components onto Integrated Circuits}},
4 author={Moore, Gordon E},
14 @article{sutter2005free,
15 title={The free lunch is over: A fundamental turn toward concurrency in software},
16 author={Sutter, Herb},
17 journal={Dr. Dobb’s Journal},
22 url = {http://www.gotw.ca/publications/concurrency-ddj.htm}
25 @article{sutter2005software,
26 author = {Herb Sutter and
28 title = {Software and the concurrency revolution},
29 journal = {ACM Queue},
34 ee = {http://doi.acm.org/10.1145/1095408.1095421},
35 bibsource = {DBLP, http://dblp.uni-trier.de}
38 @inproceedings{luebke2006gpgpu,
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},
40 title = {GPGPU: General Purpose Computation on Graphics Hardware},
41 booktitle = {ACM SIGGRAPH 2004 Course Notes},
42 series = {SIGGRAPH '04},
44 venue = {Los Angeles, CA},
46 url = {http://doi.acm.org/10.1145/1103900.1103933},
47 doi = {10.1145/1103900.1103933},
50 address = {New York, NY, USA},
53 @book{burge1975recursive,
54 title={Recursive programming techniques},
55 author={Burge, William H},
57 publisher={Addison-Wesley Reading}
60 @book{paulson1994isabelle,
61 author = {Lawrence C. Paulson},
62 title = {Isabelle - A Generic Theorem Prover},
63 publisher = {Springer-Verlag},
64 series = {Lecture Notes in Computer Science},
67 isbn = {3-540-58244-4},
68 ee = {http://dx.doi.org/10.1007/BFb0030541},
69 bibsource = {DBLP, http://dblp.uni-trier.de}
72 @phdthesis{neuper2001reactive,
73 title={Reactive User-Guidance by an Autonomous Engine Doing High-School Math},
74 author={Neuper, Walther},
76 school={Graz University of Technology}
79 @book{hammond2000research,
80 editor = {Hammond, Kevin and Michelson, Greg},
81 title = {Research Directions in Parallel Functional Programming},
84 publisher = {Springer-Verlag},
85 address = {London, UK, UK},
88 @article{hudak1989conception,
89 author = {Hudak, Paul},
90 title = {Conception, Evolution, and Application of Functional Programming Languages},
91 journal = {ACM Comput. Surv.},
92 issue_date = {Sep. 1989},
100 url = {http://doi.acm.org/10.1145/72551.72554},
101 doi = {10.1145/72551.72554},
104 address = {New York, NY, USA},
107 @article{church1932set,
108 title={A set of postulates for the foundation of logic},
109 author={Church, Alonzo},
110 journal={Annals of mathematics},
117 @article{church1940formulation,
118 author = {Alonzo Church},
119 title = {A Formulation of the Simple Theory of Types},
120 journal = {Journal of Symbolic Logic},
125 ee = {http://projecteuclid.org/euclid.jsl/1183387805},
126 bibsource = {DBLP, http://dblp.uni-trier.de}
129 @article{mccarthy1978history,
130 author = {McCarthy, John},
131 title = {History of LISP},
132 journal = {SIGPLAN Not.},
133 issue_date = {August 1978},
141 url = {http://doi.acm.org/10.1145/960118.808387},
142 doi = {10.1145/960118.808387},
145 address = {New York, NY, USA},
148 @article{backus1978can,
149 author = {John W. Backus},
150 title = {Can Programming Be Liberated From the von Neumann Style?
151 A Functional Style and its Algebra of Programs},
152 journal = {Communications of the ACM},
157 ee = {http://doi.acm.org/10.1145/359576.359579},
158 bibsource = {DBLP, http://dblp.uni-trier.de}
161 @article{milner1978theory,
162 author = {Robin Milner},
163 title = {A Theory of Type Polymorphism in Programming},
164 journal = {Journal of Computer and System Sciences},
169 ee = {http://dx.doi.org/10.1016/0022-0000(78)90014-4},
170 bibsource = {DBLP, http://dblp.uni-trier.de}
173 @book{milner1997definition,
174 author = {Milner, Robin and Tofte, Mads and Macqueen, David},
175 title = {The Definition of Standard ML},
178 publisher = {MIT Press},
179 address = {Cambridge, MA, USA},
182 @article{jones2003haskell,
183 author = {Simon {Peyton Jones} and others},
184 title = {The {Haskell} 98 Language and Libraries: The Revised Report},
185 journal = {Journal of Functional Programming},
191 url = {http://www.haskell.org/definition/},
194 @online{haskell2013functional,
195 title={Functional programming - HaskellWiki},
196 url={http://www.haskell.org/haskellwiki/Functional_programming},
200 @inproceedings{peyton1993imperative,
201 author = {Simon L. Peyton Jones and
203 title = {Imperative Functional Programming},
207 ee = {http://doi.acm.org/10.1145/158511.158524},
208 crossref = {DBLP:conf/popl/1993},
209 bibsource = {DBLP, http://dblp.uni-trier.de}
212 @article{achten1995ins,
213 author = {Peter Achten and
214 Marinus J. Plasmeijer},
215 title = {The Ins and Outs of Clean I/O},
216 journal = {Journal of Functional Programming},
221 ee = {http://dx.doi.org/10.1017/S0956796800001258},
222 bibsource = {DBLP, http://dblp.uni-trier.de}
225 @inproceedings{wadler1990linear,
226 AUTHOR = {P. Wadler},
227 TITLE = {Linear types can change the world!},
228 BOOKTITLE = {{IFIP {TC} 2} Working Conference on Programming Concepts and Methods},
229 WHERE = {{Sea of Galilee, Israel}},
230 PUBLISHER = {North Holland},
231 EDITOR = {M. Broy and C. Jones},
236 @inproceedings{launchbury1993natural,
237 author = {Launchbury, John},
238 title = {A Natural Semantics for Lazy Evaluation},
239 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
242 isbn = {0-89791-560-7},
243 venue = {Charleston, South Carolina, USA},
246 url = {http://doi.acm.org/10.1145/158511.158618},
247 doi = {10.1145/158511.158618},
250 address = {New York, NY, USA},
253 @phdthesis{lippmeier2009type,
254 title={Type Inference and Optimisation for an Impure World},
255 author={Lippmeier, Ben},
257 school={Australian National University}
260 @inproceedings{amdahl1967validity,
261 author = {Amdahl, Gene M.},
262 title = {Validity of the Single Processor Approach to Achieving Large Scale Computing Capabilities},
263 booktitle = {Proceedings of the April 18-20, 1967, Spring Joint Computer Conference},
264 series = {AFIPS '67 (Spring)},
266 venue = {Atlantic City, New Jersey},
269 url = {http://doi.acm.org/10.1145/1465482.1465560},
270 doi = {10.1145/1465482.1465560},
273 address = {New York, NY, USA},
276 @article{gustafson1988reevaluating,
277 author = {John L. Gustafson},
278 title = {Reevaluating Amdahl's Law},
279 journal = {Communications of the ACM},
284 ee = {http://doi.acm.org/10.1145/42411.42415},
285 bibsource = {DBLP, http://dblp.uni-trier.de}
288 @article{moler1986matrix,
289 title={Matrix computation on distributed memory multiprocessors},
290 author={Moler, Cleve},
291 journal={Hypercube Multiprocessors},
297 @article{geer2005chip,
298 author = {David Geer},
299 title = {Industry Trends: Chip Makers Turn to Multicore Processors},
300 journal = {IEEE Computer},
305 ee = {http://doi.ieeecomputersociety.org/10.1109/MC.2005.160},
306 bibsource = {DBLP, http://dblp.uni-trier.de}
309 @book{culler1999parallel,
310 author = {David E. Culler and
311 Jaswinder Pal Singh and
313 title = {Parallel computer architecture - a hardware / software approach},
314 publisher = {Morgan Kaufmann},
316 isbn = {978-1-55860-343-1},
317 pages = {I-XXIX, 1-1024},
318 bibsource = {DBLP, http://dblp.uni-trier.de}
321 @book{hennessy2012computer,
322 author = {John L. Hennessy and
324 title = {Computer Architecture - A Quantitative Approach (5. ed.)},
325 publisher = {Morgan Kaufmann},
327 isbn = {978-0-12-383872-8},
328 bibsource = {DBLP, http://dblp.uni-trier.de}
331 @inproceedings{tullsen1995simultaneous,
332 author = {Tullsen, Dean M. and Eggers, Susan J. and Levy, Henry M.},
333 title = {Simultaneous Multithreading: Maximizing On-chip Parallelism},
334 booktitle = {Proceedings of the 22nd Annual International Symposium on Computer Architecture},
337 isbn = {0-89791-698-0},
338 venue = {S. Margherita Ligure, Italy},
341 url = {http://doi.acm.org/10.1145/223982.224449},
342 doi = {10.1145/223982.224449},
345 address = {New York, NY, USA},
348 @article{moore2008multicore,
349 title={Multicore is bad news for supercomputers},
350 author={Moore, Samuel K},
351 journal={Spectrum, IEEE},
360 @inproceedings{li2007efficient,
361 author = {Li, Tong and Baumberger, Dan and Koufaty, David A. and Hahn, Scott},
362 title = {Efficient Operating System Scheduling for Performance-Asymmetric Multi-Core Architectures},
363 booktitle = {Proceedings of the 2007 ACM/IEEE Conference on Supercomputing},
366 isbn = {978-1-59593-764-3},
367 venue = {Reno, Nevada},
368 pages = {53:1--53:11},
371 url = {http://doi.acm.org/10.1145/1362622.1362694},
372 doi = {10.1145/1362622.1362694},
375 address = {New York, NY, USA},
378 @article{henderson1986functional,
379 author = {Peter B. Henderson},
380 title = {Functional Programming, Formal Specification, and Rapid
382 journal = {IEEE Transactions on Software Engineering},
387 ee = {http://doi.ieeecomputersociety.org/10.1109/TSE.1986.6312939},
388 bibsource = {DBLP, http://dblp.uni-trier.de}
391 @inproceedings{harris2007feedback,
392 author = {Harris, Tim and Singh, Satnam},
393 title = {Feedback Directed Implicit Parallelism},
394 booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming},
397 isbn = {978-1-59593-815-2},
398 venue = {Freiburg, Germany},
401 url = {http://doi.acm.org/10.1145/1291151.1291192},
402 doi = {10.1145/1291151.1291192},
405 address = {New York, NY, USA},
406 keywords = {functional programming, haskell, implicit parallelism},
409 @article{cantrill2008real,
410 author = {Bryan Cantrill and
412 title = {Real-World Concurrency},
413 journal = {ACM Queue},
418 ee = {http://doi.acm.org/10.1145/1454456.1454462},
419 bibsource = {DBLP, http://dblp.uni-trier.de}
422 @inproceedings{thompson2005refactoring,
423 author = {Thompson, Simon},
424 title = {Refactoring Functional Programs},
425 booktitle = {Proceedings of the 5th International Conference on Advanced Functional Programming},
428 isbn = {3-540-28540-7, 978-3-540-28540-3},
429 venue = {Tartu, Estonia},
432 url = {http://dx.doi.org/10.1007/11546382_9},
433 doi = {10.1007/11546382_9},
435 publisher = {Springer-Verlag},
436 address = {Berlin, Heidelberg},
439 @inproceedings{hammer2007proposal,
440 author = {Hammer, Matthew and Acar, Umut A. and Rajagopalan, Mohan and Ghuloum, Anwar},
441 title = {A Proposal for Parallel Self-adjusting Computation},
442 booktitle = {Proceedings of the 2007 Workshop on Declarative Aspects of Multicore Programming},
445 isbn = {978-1-59593-690-5},
446 venue = {Nice, France},
449 url = {http://doi.acm.org/10.1145/1248648.1248651},
450 doi = {10.1145/1248648.1248651},
453 address = {New York, NY, USA},
454 keywords = {change propagation, dynamic dependency graphs, fork-join programs, parallel change propagation, parallelism, self-adjusting computation, series-parallel programs},
457 @inproceedings{nocker1991concurrent,
458 author = {N\"{o}cker, E. G. J. M. H. and Smesters, J. E. W. and van Eekelen, M. C. J. D. and Plasmeijer, M. J.},
459 title = {Concurrent Clean},
460 booktitle = {Proceedings on Parallel Architectures and Languages Europe: Volume II: Parallel Languages},
461 series = {PARLE '91},
463 isbn = {0-387-54152-7},
464 venue = {Eindhoven, The Netherlands},
467 url = {http://dl.acm.org/citation.cfm?id=111634.111646},
469 publisher = {Springer-Verlag New York, Inc.},
470 address = {New York, NY, USA},
473 @inproceedings{marlow2009runtime,
474 author = {Marlow, Simon and Peyton Jones, Simon and Singh, Satnam},
475 title = {Runtime Support for Multicore Haskell},
476 booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
479 isbn = {978-1-60558-332-7},
480 venue = {Edinburgh, Scotland},
483 url = {http://doi.acm.org/10.1145/1596550.1596563},
484 doi = {10.1145/1596550.1596563},
487 address = {New York, NY, USA},
488 keywords = {Haskell parallel runtime},
491 @article{nickolls2010gpu,
492 author = {John Nickolls and
494 title = {The GPU Computing Era},
495 journal = {IEEE Micro},
500 ee = {http://doi.ieeecomputersociety.org/10.1109/MM.2010.41},
501 bibsource = {DBLP, http://dblp.uni-trier.de}
504 @article{tarditi2006accelerator,
505 author = {Tarditi, David and Puri, Sidd and Oglesby, Jose},
506 title = {Accelerator: Using Data Parallelism to Program GPUs for General-purpose Uses},
507 journal = {SIGOPS Oper. Syst. Rev.},
508 issue_date = {December 2006},
516 doi = {10.1145/1168917.1168898},
520 @article{blelloch90compiling,
521 author = {Guy E. Blelloch and
523 title = {Compiling Collection-Oriented Languages onto Massively Parallel
525 journal = {Journal of Parallel and Distributed Computing},
530 ee = {http://dx.doi.org/10.1016/0743-7315(90)90087-6},
531 bibsource = {DBLP, http://dblp.uni-trier.de}
534 @inproceedings{peytonjones2008harnessing,
535 author = {Peyton Jones, Simon},
536 title = {Harnessing the Multicores: Nested Data Parallelism in Haskell},
537 booktitle = {Proceedings of the 6th Asian Symposium on Programming Languages and Systems},
538 series = {APLAS '08},
540 isbn = {978-3-540-89329-5},
541 venue = {Bangalore, India},
544 url = {http://dx.doi.org/10.1007/978-3-540-89330-1_10},
545 doi = {10.1007/978-3-540-89330-1_10},
547 publisher = {Springer-Verlag},
548 address = {Berlin, Heidelberg},
551 @inproceedings{baker1977incremental,
552 author = {Baker,Jr., Henry C. and Hewitt, Carl},
553 title = {The Incremental Garbage Collection of Processes},
554 booktitle = {Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages},
558 url = {http://doi.acm.org/10.1145/800228.806932},
559 doi = {10.1145/800228.806932},
562 address = {New York, NY, USA},
563 keywords = {Eager evaluation, Garbage collection, Lazy evaluation, Multiprocessing systems, Processor scheduling},
566 @article{halstead1985multilisp,
567 author = {Robert H. Halstead Jr.},
568 title = {Multilisp: A Language for Concurrent Symbolic Computation},
569 journal = {ACM Transactions on Programming Languages and Systems},
574 ee = {http://doi.acm.org/10.1145/4472.4478},
575 bibsource = {DBLP, http://dblp.uni-trier.de}
578 @inproceedings{matthews2010efficient,
579 author = {Matthews, David C.J. and Wenzel, Makarius},
580 title = {Efficient Parallel Programming in Poly/ML and Isabelle/ML},
581 booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming},
584 isbn = {978-1-60558-859-9},
585 venue = {Madrid, Spain},
588 url = {http://doi.acm.org/10.1145/1708046.1708058},
589 doi = {10.1145/1708046.1708058},
592 address = {New York, NY, USA},
593 keywords = {data parallelism, isabelle, parallel standard ml, poly/ml, theorem proving applications},
596 @article{wegner1990concepts,
597 author = {Peter Wegner},
598 title = {Concepts and paradigms of object-oriented programming},
599 journal = {OOPS Messenger},
604 ee = {http://doi.acm.org/10.1145/382192.383004},
605 bibsource = {DBLP, http://dblp.uni-trier.de}
608 @article{shavit1997software,
609 title={Software transactional memory},
610 author={Shavit, Nir and Touitou, Dan},
611 journal={Distributed Computing},
616 publisher={Springer-Verlag}
619 @article{herlihy1990linearizability,
620 author = {Herlihy, Maurice P. and Wing, Jeannette M.},
621 title = {Linearizability: A Correctness Condition for Concurrent Objects},
622 journal = {ACM Trans. Program. Lang. Syst.},
623 issue_date = {July 1990},
631 url = {http://doi.acm.org/10.1145/78969.78972},
632 doi = {10.1145/78969.78972},
635 address = {New York, NY, USA},
638 @inproceedings{ramadan2009committing,
639 author = {Ramadan, Hany E. and Roy, Indrajit and Herlihy, Maurice and Witchel, Emmett},
640 title = {Committing Conflicting Transactions in an STM},
641 booktitle = {Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
642 series = {PPoPP '09},
644 isbn = {978-1-60558-397-6},
645 venue = {Raleigh, NC, USA},
648 url = {http://doi.acm.org/10.1145/1504176.1504201},
649 doi = {10.1145/1504176.1504201},
652 address = {New York, NY, USA},
653 keywords = {concurrency control, dependence-aware, serializability, transactional memory},
656 @inproceedings{herlihy2003software,
657 author = {Herlihy, Maurice and Luchangco, Victor and Moir, Mark and Scherer,III, William N.},
658 title = {Software Transactional Memory for Dynamic-sized Data Structures},
659 booktitle = {Proceedings of the Twenty-second Annual Symposium on Principles of Distributed Computing},
662 isbn = {1-58113-708-7},
663 venue = {Boston, Massachusetts},
666 url = {http://doi.acm.org/10.1145/872035.872048},
667 doi = {10.1145/872035.872048},
670 address = {New York, NY, USA},
673 @patent{zhang2010software,
674 title={Software Transaction Commit Order and Conflict Management},
675 author={Zhang, L. and Grover, V.K. and Magruder, M.M. and Detlefs, D. and Duffy, J.J. and Graefe, G.},
676 url={http://www.google.co.in/patents/US7711678},
682 @techreport{ennals2006software,
683 title={Software transactional memory should not be obstruction-free},
684 author={Ennals, Robert},
686 institution={Technical Report IRC-TR-06-052, Intel Research Cambridge Tech Report}
689 @techreport{ennals2005efficient,
690 author = {Ennals, Robert},
691 title = {Efficient Software Transactional Memory},
692 institution = {Intel Research Cambridge Tech Report},
693 number = {IRC-TR-05-051},
694 pdf = {http://www.cs.wisc.edu/trans-memory/misc-papers/051_Rob_Ennals.pdf},
699 @inproceedings{saha2006mcrt,
700 author = {Saha, Bratin and Adl-Tabatabai, Ali-Reza and Hudson, Richard L. and Minh, Chi Cao and Hertzberg, Benjamin},
701 title = {McRT-STM: A High Performance Software Transactional Memory System for a Multi-Core Runtime},
702 booktitle = {Proceedings of the Eleventh ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
703 series = {PPoPP '06},
705 isbn = {1-59593-189-9},
708 doi = {10.1145/1122971.1123001},
712 @inproceedings{harris2005composable,
713 author = {Harris, Tim and Marlow, Simon and Peyton-Jones, Simon and Herlihy, Maurice},
714 title = {Composable Memory Transactions},
715 booktitle = {Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
716 series = {PPoPP '05},
718 isbn = {1-59593-080-9},
719 venue = {Chicago, IL, USA},
722 url = {http://doi.acm.org/10.1145/1065944.1065952},
723 doi = {10.1145/1065944.1065952},
726 address = {New York, NY, USA},
727 keywords = {locks, non-blocking algorithms, transactions},
730 @inproceedings{hewitt1973universal,
731 author = {Hewitt, Carl and Bishop, Peter and Steiger, Richard},
732 title = {A Universal Modular ACTOR Formalism for Artificial Intelligence},
733 booktitle = {Proceedings of the 3rd International Joint Conference on Artificial Intelligence},
736 venue = {Stanford, USA},
739 url = {http://dl.acm.org/citation.cfm?id=1624775.1624804},
741 publisher = {Morgan Kaufmann Publishers Inc.},
742 address = {San Francisco, CA, USA},
745 @article{hewitt1977viewing,
746 author = {Carl Hewitt},
747 title = {Viewing Control Structures as Patterns of Passing Messages},
748 journal = {Artificial Intelligence},
753 ee = {http://dx.doi.org/10.1016/0004-3702(77)90033-9},
754 bibsource = {DBLP, http://dblp.uni-trier.de}
757 @article{agha1985actors,
758 author = {Gul A. Agha},
759 title = {ACTORS - a model of concurrent computation in distributed
761 publisher = {MIT Press},
762 series = {MIT Press series in artificial intelligence},
764 isbn = {978-0-262-01092-4},
765 pages = {I-IX, 1-144},
766 bibsource = {DBLP, http://dblp.uni-trier.de}
769 @article{agha1997foundation,
770 author = {Gul Agha and
774 title = {A Foundation for Actor Computation},
775 journal = {Journal of Functional Programming},
780 ee = {http://journals.cambridge.org/action/displayAbstract?aid=44065},
781 bibsource = {DBLP, http://dblp.uni-trier.de}
785 title={Akka framework},
786 author={Thurau, Martin},
788 howpublished={Paper for Seminar Software Systems Engineering, Universität zu Lübeck},
789 url={http://media.itm.uni-luebeck.de/teaching/ws2012/sem-sse/martin-thurau-akka.io.pdf}
792 @inproceedings{karmani2009actor,
793 author = {Karmani, Rajesh K. and Shali, Amin and Agha, Gul},
794 title = {Actor Frameworks for the JVM Platform: A Comparative Analysis},
795 booktitle = {Proceedings of the 7th International Conference on Principles and Practice of Programming in Java},
798 isbn = {978-1-60558-598-7},
799 venue = {Calgary, Alberta, Canada},
802 url = {http://doi.acm.org/10.1145/1596655.1596658},
803 doi = {10.1145/1596655.1596658},
806 address = {New York, NY, USA},
807 keywords = {JVM, Java, abstractions, actors, comparison, frameworks, libraries, performance, semantics},
810 @article{fuggetta1998understanding,
811 author = {Alfonso Fuggetta and
812 Gian Pietro Picco and
814 title = {Understanding Code Mobility},
815 journal = {IEEE Transactions on Software Engineering},
820 ee = {http://doi.ieeecomputersociety.org/10.1109/32.685258},
821 bibsource = {DBLP, http://dblp.uni-trier.de}
824 @article{panwar1994methodology,
825 author = {Rajendra Panwar and
827 title = {A Methodology for Programming Scalable Architectures},
828 journal = {Journal of Parallel and Distributed Computing},
833 ee = {http://dx.doi.org/10.1006/jpdc.1994.1105},
834 bibsource = {DBLP, http://dblp.uni-trier.de}
837 @techreport{odersky2004overview,
838 title={An overview of the Scala programming language},
839 author={Martin Odersky and Vincent Cremet and Iulian Dragos and Gilles Dubochet and Burak Emir and Sean McDirmid and Stéphane Micheloud and Nikolay Mihaylov and Michel Schinz and Erik Stenman and Lex Spoon and Matthias Zenger},
841 institution={École Polytechnique Fédérale de Lausanne},
842 address={1015 Lausanne, Switzerland},
843 number={LAMP-REPORT-2006-001},
847 @incollection{haller2006event,
848 title={Event-based programming without inversion of control},
849 author={Haller, Philipp and Odersky, Martin},
850 booktitle={Modular Programming Languages},
853 publisher={Springer-Verlag}
856 @article{haller2009scala,
857 title={Scala actors: Unifying thread-based and event-based programming},
858 author={Haller, Philipp and Odersky, Martin},
859 journal={Theoretical Computer Science},
867 @online {akka2014futures,
868 title={Futures (Scala) -- Akka Documentation},
869 url={http://doc.akka.io/docs/akka/current/scala/futures.html},
870 urldate={2014-06-05},
874 @online {scala2014migration,
875 title={The Scala Actors Migration Guide - Scala Documentation},
876 author={Jovanovic, Vojin and Haller, Philipp},
877 url={http://docs.scala-lang.org/overviews/core/actors-migration-guide.html},
881 @inproceedings{tasharofi2013scala,
882 author = {Tasharofi, Samira and Dinges, Peter and Johnson, Ralph E.},
883 title = {Why Do Scala Developers Mix the Actor Model with Other Concurrency Models?},
884 booktitle = {Proceedings of the 27th European Conference on Object-Oriented Programming},
887 isbn = {978-3-642-39037-1},
888 venue = {Montpellier, France},
891 url = {http://dx.doi.org/10.1007/978-3-642-39038-8_13},
892 doi = {10.1007/978-3-642-39038-8_13},
894 publisher = {Springer-Verlag},
895 address = {Berlin, Heidelberg},
898 @article{hoare1978communicating,
899 author = {C. A. R. Hoare},
900 title = {Communicating Sequential Processes},
901 journal = {Communications of the ACM},
906 ee = {http://doi.acm.org/10.1145/359576.359585},
907 bibsource = {DBLP, http://dblp.uni-trier.de}
911 author = {{INMOS, Ltd.}},
913 address = {Englewood Cliffs},
914 publisher = {Prentice Hall},
915 title = {The occam programming manual}
918 @inproceedings{dorward1997programming,
919 author = {Dorward, Sean and Pike, Rob and Winterbottom, Phil},
920 title = {Programming in Limbo},
921 booktitle = {Proceedings of the 42Nd IEEE International Computer Conference},
922 series = {COMPCON '97},
924 isbn = {0-8186-7804-6},
926 url = {http://dl.acm.org/citation.cfm?id=792770.793719},
928 publisher = {IEEE Computer Society},
929 address = {Washington, DC, USA},
930 keywords = {programming languages, modules, graphics},
933 @inproceedings{pike2012go,
935 title = {Go at Google},
936 booktitle = {Proceedings of the Conference on Systems, Programming, and Applications: Software
940 ee = {http://doi.acm.org/10.1145/2384716.2384720},
941 bibsource = {DBLP, http://dblp.uni-trier.de},
942 venue = {Tucson, AZ, USA},
943 editor = {Gary T. Leavens}
946 @inproceedings{brown2012paraforming,
947 author = {Brown, Christopher and Loidl, Hans-Wolfgang and Hammond, Kevin},
948 title = {ParaForming: Forming Parallel Haskell Programs Using Novel Refactoring Techniques},
949 booktitle = {Proceedings of the 12th International Conference on Trends in Functional Programming},
952 isbn = {978-3-642-32036-1},
953 venue = {Madrid, Spain},
956 url = {http://dx.doi.org/10.1007/978-3-642-32037-8_6},
957 doi = {10.1007/978-3-642-32037-8_6},
959 publisher = {Springer-Verlag},
960 address = {Berlin, Heidelberg},
963 @article{kennedy1991interactive,
964 author = {Ken Kennedy and
965 Kathryn S. McKinley and
967 title = {Interactive Parallel Programming using the ParaScope Editor},
968 journal = {IEEE Transactions on Parallel and Distributed Systems},
973 ee = {http://doi.ieeecomputersociety.org/10.1109/71.86108},
974 bibsource = {DBLP, http://dblp.uni-trier.de}
977 @inproceedings{wloka2009refactoring,
978 author = {Wloka, Jan and Sridharan, Manu and Tip, Frank},
979 title = {Refactoring for Reentrancy},
980 booktitle = {Proceedings of the the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering},
981 series = {ESEC/FSE '09},
983 isbn = {978-1-60558-001-2},
984 venue = {Amsterdam, The Netherlands},
987 url = {http://doi.acm.org/10.1145/1595696.1595723},
988 doi = {10.1145/1595696.1595723},
991 address = {New York, NY, USA},
992 keywords = {program transformation, reentrant code, refactoring},
995 @article{dig2011refactoring,
996 author = {Danny Dig},
997 title = {A Refactoring Approach to Parallelism},
998 journal = {IEEE Software},
1003 ee = {http://doi.ieeecomputersociety.org/10.1109/MS.2011.1},
1004 bibsource = {DBLP, http://dblp.uni-trier.de}
1007 @article{brown2013cost,
1008 author = {Christopher Brown and
1011 Peter Kilpatrick and
1013 title = {Cost-Directed Refactoring for Parallel Erlang Programs},
1014 journal = {International Journal of Parallel Programming},
1019 ee = {http://dx.doi.org/10.1007/s10766-013-0266-5},
1020 bibsource = {DBLP, http://dblp.uni-trier.de}
1023 @inproceedings{brown2012language,
1024 author = {Brown, Christopher and Hammond, Kevin and Danelutto, Marco and Kilpatrick, Peter},
1025 title = {A Language-Independent Parallel Refactoring Framework},
1026 booktitle = {Proceedings of the Fifth Workshop on Refactoring Tools},
1029 isbn = {978-1-4503-1500-5},
1030 venue = {Rapperswil, Switzerland},
1033 url = {http://doi.acm.org/10.1145/2328876.2328884},
1034 doi = {10.1145/2328876.2328884},
1037 address = {New York, NY, USA},
1038 keywords = {C/C++, Erlang, ParaPhrase, concurrency, parallelism, patterns, refactoring, skeletons},
1041 @incollection{hammond2013paraphrase,
1043 isbn={978-3-642-35886-9},
1044 booktitle={Formal Methods for Components and Objects},
1046 series={Lecture Notes in Computer Science},
1047 editor={Beckert, Bernhard and Damiani, Ferruccio and de Boer, FrankS. and Bonsangue, MarcelloM.},
1048 doi={10.1007/978-3-642-35887-6_12},
1049 title={The ParaPhrase Project: Parallel Patterns for Adaptive Heterogeneous Multicore Systems},
1050 url={http://dx.doi.org/10.1007/978-3-642-35887-6_12},
1051 publisher={Springer-Verlag},
1052 address={Berlin, Heidelberg},
1053 author={Hammond, Kevin and Aldinucci, Marco and Brown, Christopher and Cesarini, Francesco and Danelutto, Marco and González-Vélez, Horacio and Kilpatrick, Peter and Keller, Rainer and Rossbory, Michael and Shainer, Gilad},
1058 @inproceedings{li2006comparative,
1059 author = {Li, Huiqing and Thompson, Simon},
1060 title = {Comparative Study of Refactoring Haskell and Erlang Programs},
1061 booktitle = {Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation},
1062 series = {SCAM '06},
1064 isbn = {0-7695-2353-6},
1067 url = {http://dx.doi.org/10.1109/SCAM.2006.8},
1068 doi = {10.1109/SCAM.2006.8},
1070 publisher = {IEEE Computer Society},
1071 address = {Washington, DC, USA},
1074 @article{hindley1969principal,
1075 author = {Hindley, R.},
1076 doi = {10.2307/1995158},
1078 journal = {Transactions of the American Mathematical Society},
1080 publisher = {American Mathematical Society},
1081 title = {{The Principal Type-Scheme of an Object in Combinatory Logic}},
1086 @inproceedings{milner1975logic,
1087 title={{A Logic for Computable Functions with Reflexive and Polymorphic Types}},
1088 author={Milner, Robin and Morris, Lockwood and Newey, Malcolm},
1090 booktitle = {Proceedings of the Conference on Proving and Improving Programs}
1093 @phdthesis{damas1984type,
1094 title={Type assignment in programming languages.},
1095 author={Damas, Luis Manuel Martins},
1097 school={University of Edinburgh}
1100 @article{paulson1989foundation,
1101 author = {Lawrence C. Paulson},
1102 title = {The Foundation of a Generic Theorem Prover},
1103 journal = {Journal of Automated Reasoning},
1108 ee = {http://dx.doi.org/10.1007/BF00248324},
1109 bibsource = {DBLP, http://dblp.uni-trier.de}
1112 @inproceedings{weeks2006whole,
1113 author = {Weeks, Stephen},
1114 title = {Whole-program Compilation in MLton},
1115 booktitle = {Proceedings of the 2006 Workshop on ML},
1118 isbn = {1-59593-483-9},
1119 venue = {Portland, Oregon, USA},
1122 url = {http://doi.acm.org/10.1145/1159876.1159877},
1123 doi = {10.1145/1159876.1159877},
1126 address = {New York, NY, USA},
1129 @online{smlnj2013standard,
1130 url={http://www.smlnj.org/},
1131 title={Standard ML of New Jersey},
1132 author={SML/NJ Fellowship, The},
1133 urldate={2014-05-15}
1136 @online{romanenko2014moscow,
1137 url={http://mosml.org/},
1142 @online{matthews2014documentation,
1143 url={http://polyml.org/Doc.html},
1144 title={Documentation},
1145 author={Matthews, David C.J.},
1149 @techreport{matthews1995papers,
1150 author = {Matthews, David CJ},
1151 title = {{Papers on Poly/ML}},
1154 institution = {Computer Laboratory, University of Cambridge}
1157 @techreport{matthews1991distributed,
1158 title={A Distributed Concurrent Implementation of Standard ML},
1159 author={Matthews, David CJ},
1161 institution={LFCS, Department of Computer Science, University of Edinburgh}
1164 @inproceedings{reppy1993concurrent,
1165 author = {Reppy, John H.},
1166 title = {Concurrent ML: Design, Application and Semantics},
1167 booktitle = {Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992},
1168 venue={McMaster University, Hamilton, Ontario, Canada},
1170 isbn = {3-540-56883-2},
1173 publisher = {Springer-Verlag}
1176 @manual{wenzel2013isar,
1177 title={The Isabelle/Isar Reference Manual},
1178 author={Wenzel, Makarius and others},
1180 url={http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf}
1183 @incollection{wenzel1999isar,
1185 series={Lecture Notes in Computer Science},
1186 editor={Bertot, Yves and Dowek, Gilles and Théry, Laurent and Hirschowitz, André and Paulin, Christine},
1187 doi={10.1007/3-540-48256-3_12},
1188 title={Isar — A Generic Interpretative Approach to Readable Formal Proof Documents},
1189 author={Wenzel, Makarius},
1190 booktitle={Theorem Proving in Higher Order Logics},
1193 publisher={Springer-Verlag},
1194 address={Berlin, Heidelberg},
1195 isbn={978-3-540-66463-5}
1198 @inproceedings{wenzel2014uipide,
1199 title={Asynchronous User Interaction and Tool Integration in Isabelle/PIDE},
1200 author={Wenzel, Makarius},
1203 booktitle={Proceedings of the 5th Int.\ Conference on Interactive Theorem Proving},
1204 venue={Vienna, Austria},
1205 editor = {Klein, G and Gamboa, R}
1208 @inproceedings{matichuk2014isabelle,
1209 author = {Matichuk, Daniel and Wenzel, Makarius and Murray, Toby},
1212 title = {An Isabelle Proof Method Language},
1213 booktitle={Proceedings of the 5th Int.\ Conference on Interactive Theorem Proving},
1214 publisher = {Springer-Verlag},
1215 venue={Vienna, Austria},
1216 editor = {Klein, G and Gamboa, R}
1219 @article{wenzel2012asynchronous,
1220 author = {Makarius Wenzel},
1221 title = {Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit},
1222 journal = {Electronic Notes in Theoretical Computer Science},
1228 @manual{wenzel2013isabelle,
1229 title={The Isabelle System Manual},
1230 author={Wenzel, Makarius and Berghofer, Stefan},
1232 url={http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/system.pdf}
1235 @inproceedings{wenzel2011isabelle,
1236 author = {Wenzel, Makarius},
1237 title = {Isabelle As Document-Oriented Proof Assistant},
1238 booktitle = {Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics},
1241 isbn = {978-3-642-22672-4},
1242 venue = {Bertinoro, Italy},
1245 url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
1247 publisher = {Springer-Verlag},
1248 address = {Berlin, Heidelberg},
1251 @inproceedings{wenzel2012isabelle,
1252 author = {Wenzel, Makarius},
1253 title = {Isabelle/jEdit: A Prover IDE Within the PIDE Framework},
1254 booktitle = {Proceedings of the 11th International Conference on Intelligent Computer Mathematics},
1257 isbn = {978-3-642-31373-8},
1258 venue = {Bremen, Germany},
1261 url = {http://dx.doi.org/10.1007/978-3-642-31374-5_38},
1262 doi = {10.1007/978-3-642-31374-5_38},
1264 publisher = {Springer-Verlag},
1265 address = {Berlin, Heidelberg},
1268 @manual{wenzel2013jedit,
1269 title={Isabelle/jEdit},
1270 author={Wenzel, Makarius},
1272 url={http://isabelle.in.tum.de/dist/doc/jedit.pdf}
1275 @book{chlipala2011certified,
1276 author = {Chlipala, Adam},
1277 title = {Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant},
1279 isbn = {0262026651, 9780262026659},
1280 publisher = {The MIT Press},
1283 @book{nipkow2002isabelle,
1284 author = {Nipkow, Tobias and Wenzel, Makarius and Paulson, Lawrence C.},
1285 title = {Isabelle/HOL: A Proof Assistant for Higher-order Logic},
1288 isbn = {3-540-43376-7},
1289 publisher = {Springer-Verlag}
1292 @manual{wenzel2013impl,
1293 title={The Isabelle/Isar Implementation},
1294 author={Wenzel, Makarius},
1296 note={With contributions by Florian Haftmann and Larry Paulson},
1297 url={http://isabelle.in.tum.de/doc/implementation.pdf}
1300 @book{van1979checking,
1301 title = {Checking Landau's ``Grundlagen'' in the Automath system},
1302 author = {van Benthem Jutting, L. S.},
1303 publisher = {Mathematisch Centrum},
1304 address = {Eindhoven},
1308 @article{landin1966next,
1309 author = {Peter J. Landin},
1310 title = {The next 700 programming languages},
1311 journal = {Communications of the ACM},
1318 @inproceedings{paulson1988isabelle,
1319 author = {Paulson, Lawrence C.},
1320 title = {Isabelle: The Next Seven Hundred Theorem Provers},
1321 booktitle = {Proceedings of the 9th International Conference on Automated Deduction},
1323 isbn = {3-540-19343-X},
1326 url = {http://dl.acm.org/citation.cfm?id=648228.751990},
1328 publisher = {Springer-Verlag},
1329 address = {London, UK, UK},
1332 @article{gentzen1964investigations,
1333 title={Investigations into logical deduction},
1334 author={Gentzen, Gerhard},
1335 journal={American philosophical quarterly},
1343 @article{coquand1988calculus,
1344 author = {Thierry Coquand and
1345 G{\'e}rard P. Huet},
1346 title = {The Calculus of Constructions},
1347 journal = {Information and Computation},
1352 ee = {http://dx.doi.org/10.1016/0890-5401(88)90005-3},
1353 bibsource = {DBLP, http://dblp.uni-trier.de}
1356 @article{fitzgerald2008vdmtools,
1357 author = {John S. Fitzgerald and
1358 Peter Gorm Larsen and
1360 title = {VDMTools: advances in support for formal modeling in VDM},
1361 journal = {SIGPLAN Notices},
1366 ee = {http://doi.acm.org/10.1145/1361213.1361214},
1367 bibsource = {DBLP, http://dblp.uni-trier.de}
1370 @incollection{fitzgerald2008vienna,
1371 title = {Vienna Development Method},
1372 author = {Fitzgerald, John S. and Larsen, Peter Gorm and Verhoef, Marcel},
1373 publisher = {John Wiley \& Sons, Inc.},
1374 isbn = {9780470050118},
1375 url = {http://dx.doi.org/10.1002/9780470050118.ecse447},
1376 doi = {10.1002/9780470050118.ecse447},
1377 booktitle = {Wiley Encyclopedia of Computer Science and Engineering},
1381 @book{bjorner2006software,
1382 title={Software Engineering},
1383 author={Bj{\o}rner, Dines},
1386 series={Texts in Theoretical Computer Science},
1387 publisher={Springer-Verlag}
1390 @article{back2010structured,
1391 author = {Ralph-Johan Back},
1392 title = {Structured derivations: a unified proof style for teaching mathematics},
1393 journal = {Formal Aspects of Computing},
1400 @article{wenzel2007generic,
1401 title={Isabelle/Isar -- a generic framework for human-readable proof documents},
1402 author={Wenzel, Makarius},
1403 journal={From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec},
1410 @inproceedings{neuper2012automated,
1411 author = {Walther Neuper},
1412 title = {Automated Generation of User Guidance by Combining Computation
1414 editor = {Pedro Quaresma and
1416 booktitle = {Proceedings of the First Workshop on CTP Components for Educational
1417 Software (THedu'11)},
1422 venue = {Wroclaw, Poland},
1426 @article{daroczy2013error,
1427 title={Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
1428 author={Dar{\'o}czy, Gabriella and Neuper, Walther},
1429 journal={Electronic Journal of Mathematics \& Technology},
1435 @mastersthesis{kienleitner2012towards,
1436 title={Towards ``NextStep Userguidance'' in a Mechanized Math Assistant},
1437 author={Kienleitner, Markus},
1438 school={Graz University of Technology},
1440 type={Bachelor's thesis}
1443 @inproceedings{wenzel2009parallel,
1444 author = {Makarius Wenzel},
1445 title = {{Parallel Proof Checking in {Isabelle/Isar}}},
1446 booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)},
1448 editor = {Dos Reis, G and L Th\'ery},
1449 publisher = {ACM Digital Library}
1452 @techreport{buchberger1984mathematik,
1453 author={Buchberger, Bruno},
1454 title={Mathematik für Informatiker II (Problemlösestrategien und Algorithmentypen)},
1455 institution={RISC-Linz},
1456 type={Lecture notes},
1457 number={CAMP-Publ.-No. 84-4.0},
1461 @mastersthesis{lehnfeld2011verbindung,
1462 title={Verbindung von 'Computation' und 'Deduction' im \isac{}-System},
1463 author={Lehnfeld, Mathias},
1464 school={Technische Universität Wien},
1466 type={Bachelor's project report}
1469 @phdthesis{krauss2009automating,
1470 author = {Alexander Krauss},
1471 title = {Automating recursive definitions and termination proofs
1472 in higher-order logic},
1475 school = {Technische Universität München},
1476 ee = {http://mediatum2.ub.tum.de/doc/681651/document.pdf},
1477 bibsource = {DBLP, http://dblp.uni-trier.de}
1480 @mastersthesis{rocnik2012interactive,
1481 author={Jan Rocnik},
1482 title={Interactive Course Material for Signal Processing based on Isabelle/\isac{}},
1483 type={Bachelor's thesis},
1485 url={http://www.ist.tugraz.at/projects/isac/publ/jrocnik_bakk.pdf},
1486 school={Graz University of Technology}
1489 @inproceedings{haftmann2010code,
1490 author = {Haftmann, Florian and Nipkow, Tobias},
1491 title = {Code Generation via Higher-order Rewrite Systems},
1492 booktitle = {Proceedings of the 10th International Conference on Functional and Logic Programming},
1493 series = {FLOPS'10},
1495 isbn = {3-642-12250-7, 978-3-642-12250-7},
1496 venue = {Sendai, Japan},
1499 url = {http://dx.doi.org/10.1007/978-3-642-12251-4_9},
1500 doi = {10.1007/978-3-642-12251-4_9},
1502 publisher = {Springer-Verlag},
1503 address = {Berlin, Heidelberg},
1506 @book{charniak2014artificial,
1507 author = {Charniak, Eugene and Riesbeck, Christopher K. and McDermott, Drew V. and Meehan, James R.},
1508 title = {Artificial Intelligence Programming},
1510 isbn = {0898596092},
1512 publisher = {Psychology Press}
1515 @inproceedings{aspinall2000proof,
1516 author = {Aspinall, David},
1517 title = {Proof General: A Generic Tool for Proof Development},
1518 booktitle = {Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held As Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000},
1519 series = {TACAS '00},
1521 isbn = {3-540-67282-6},
1524 url = {http://dl.acm.org/citation.cfm?id=646484.691773},
1526 publisher = {Springer-Verlag},
1527 address = {London, UK, UK},
1530 @book{simon1965shape,
1531 address = {New York},
1532 author = {Simon, H. A.},
1533 publisher = {Harper \& Row},
1534 title = {{The Shape of Automation for Men and Management}},
1538 @book{gordon1993introduction,
1539 title={Introduction to HOL: A theorem proving environment for higher-order logic},
1540 author={Gordon, Michael JC and Melham, Tom F},
1542 publisher={Cambridge University Press}
1545 @online{harrison2014hol,
1546 author={Harrison, John},
1548 urldate={2014-05-26},
1549 url={http://www.cl.cam.ac.uk/~jrh13/hol-light/}
1552 @article{appel1977solution,
1553 title={The solution of the four-color-map problem},
1554 author={Appel, Kenneth and Haken, Wolfgang},
1555 journal={Scientific American},
1561 @incollection{hales2011historical,
1563 isbn={978-1-4614-1128-4},
1564 booktitle={The Kepler Conjecture},
1565 editor={Lagarias, Jeffrey C.},
1566 doi={10.1007/978-1-4614-1129-1_3},
1567 title={Historical Overview of the Kepler Conjecture},
1568 url={http://dx.doi.org/10.1007/978-1-4614-1129-1_3},
1569 publisher={Springer New York},
1570 author={Hales, ThomasC.},
1575 @techreport{sharangpani1994statistical,
1576 title={Statistical Analysis of Floating Point Flaw in the Pentium Processor},
1577 author={Sharangpani, HP and Barton, ML},
1578 institution={Intel Corporation},
1582 @online{intel1997intel,
1584 title={Intel® Pentium® Processor - Invalid Instruction Erratum Overview},
1585 urldate={2014-05-26},
1586 url={http://www.intel.com/support/processors/pentium/ppiie/index.htm}
1589 @article{brandt2007theorem,
1590 title={Theorem Proving in Higher Order Logics},
1591 author={Brandt, Klaus Schneider Jens},
1593 publisher={Springer-Verlag}
1596 @online{isabelle2013news,
1597 title={isabelle.in.tum.de/dist/Isabelle2013-2/NEWS},
1598 url={http://isabelle.in.tum.de/dist/Isabelle2013-2/NEWS},
1599 urldate={2014-05-27},
1603 @online{isac2014knowledge,
1604 title={www.ist.tugraz.at/projects/isac/www/kbase/thy/index\_thy.html},
1605 url={http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html},
1606 urldate={2014-06-01}
1609 @online{isac2014pbl,
1610 title={www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html},
1611 url={http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html},
1612 urldate={2014-06-01}
1615 @online{isac2014met,
1616 title={www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html},
1617 url={http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html},
1618 urldate={2014-06-01}
1621 @manual{krauss2013defining,
1622 title={Defining recursive functions in Isabelle/HOL},
1623 author={Krauss, Alexander},
1625 url={http://isabelle.in.tum.de/doc/functions.pdf}
1628 @online{google2012flyspeck,
1629 title={FlyspeckFactSheet},
1630 url={https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet},
1631 urldate={2014-06-01},
1635 @online{austriaforum2014zemanek,
1636 title={Zemanek, Heinz | Austria-Forum > Biographien},
1637 url={http://austria-forum.org/af/Wissenssammlungen/Biographien/Zemanek,_Heinz},
1638 urldate={2014-06-02}
1641 @article{gonthier2008formal,
1642 title={Formal Proof --- The Four Colour Theorem},
1643 author={Gonthier, Georges},
1644 journal={Notices of the AMS},
1651 @online{pipermail2014clisa,
1652 title={The Cl-isabelle-users Archives},
1653 url={https://lists.cam.ac.uk/pipermail/cl-isabelle-users/},
1654 urldate={2014-06-05},
1658 @online{tum2013team,
1660 url={http://www21.in.tum.de/team},
1661 urldate={2014-06-05},
1665 @online{tum2014isainst,
1666 title={Installation},
1667 url={http://isabelle.in.tum.de/installation.html},
1668 urldate={2014-06-05},
1672 @online{andriusvelykis2013isaclipse,
1673 title={Isabelle/Eclipse},
1674 url={http://andriusvelykis.github.io/isabelle-eclipse/},
1675 urldate={2014-06-05},
1679 @online{emath2013emath,
1681 url={http://emath.eu/en/},
1682 urldate={2014-06-05},
1686 @online{tum2013isadoc,
1687 title={Documentation},
1688 url={http://isabelle.in.tum.de/documentation.html},
1689 urldate={2014-06-13},
1691 OPTnote={Theory libraries for Isabelle2013-2}
1694 @online{wiki2014proofass,
1695 title={Proof assistant - Wikipedia, the free encyclopedia},
1696 url={http://en.wikipedia.org/wiki/Proof_assistant},
1697 urldate={2014-06-13},
1701 @online{wiki2014atp,
1702 title={Automated theorem proving - Wikipedia, the free encyclopedia},
1703 url={http://en.wikipedia.org/wiki/Automated_theorem_proving},
1704 urldate={2014-06-13},
1708 @online{tum2013isahol,
1709 title={Isabelle/HOL sessions},
1710 url={http://isabelle.in.tum.de/dist/library/HOL/},
1711 urldate={2014-06-13}
1714 @online{isac2014pblequuniv,
1715 title={www.ist.tugraz.at/projects/isac/www/kbase/pbl/pbl\_equ\_univ.html},
1716 url={http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/pbl_equ_univ.html},
1717 urldate={2014-06-13}
1720 @mastersthesis{haller2006object,
1721 title={An Object-Oriented Programming Model for Event-Based Actors},
1722 author={Haller, Philipp},
1724 school={University of Karlsruhe}
1727 @online{wenzel2014actors,
1728 title={Re: [isabelle-dev] scala-2.11.0},
1729 url={http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg05253.html},
1730 author={Wenzel, Makarius},
1732 urldate={2014-06-16}
1735 @inproceedings{blanchette2011automatic,
1736 author = {Blanchette, Jasmin Christian and Bulwahn, Lukas and Nipkow, Tobias},
1737 title = {Automatic Proof and Disproof in Isabelle/HOL},
1738 booktitle = {Proceedings of the 8th International Conference on Frontiers of Combining Systems},
1739 series = {FroCoS'11},
1741 isbn = {978-3-642-24363-9},
1742 venue = {Saarbrücken, Germany},
1745 url = {http://dl.acm.org/citation.cfm?id=2050784.2050787},
1747 publisher = {Springer-Verlag},
1748 address = {Berlin, Heidelberg},
1751 %@inproceedings{wenzel2007sml,
1752 % title={SML with antiquotations embedded into Isabelle/Isar},
1753 % author={Wenzel, Makarius and Chaieb, Amine},
1754 % booktitle={Workshop on Programming Languages for Mechanized Mathematics (satellite of CALCULEMUS 2007). %Hagenberg, Austria},
1758 @online{tum2014repo,
1759 title={isabelle: Summary},
1760 url={http://isabelle.in.tum.de/repos/isabelle/},
1762 urldate={2014-06-21}