@article{moore1965cramming,

   title={{Cramming More Components onto Integrated Circuits}},

   author={Moore, Gordon E.},

   year={1965},

   journal={Electronics},

   pages = {114--117},

   month = {apr},

   day = {19},

   number={8},

   volume={38}

 }

 @article{sutter2005free,

   title={The free lunch is over: A fundamental turn toward concurrency in software},

   author={Sutter, Herb},

   journal={Dr. Dobb’s Journal},

   volume={30},

   number={3},

   pages={202--210},

   year={2005},

   url = {http://www.gotw.ca/publications/concurrency-ddj.htm}

 }

 @article{sutter2005software,

   author    = {Herb Sutter and

                James R. Larus},

   title     = {Software and the concurrency revolution},

   journal   = {ACM Queue},

   volume    = {3},

   number    = {7},

   year      = {2005},

   pages     = {54-62},

   ee        = {http://doi.acm.org/10.1145/1095408.1095421},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{luebke2006gpgpu,

  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},

  title = {GPGPU: General Purpose Computation on Graphics Hardware},

  booktitle = {ACM SIGGRAPH 2004 Course Notes},

  series = {SIGGRAPH '04},

  year = {2004},

  venue = {Los Angeles, CA},

  articleno = {33},

  url = {http://doi.acm.org/10.1145/1103900.1103933},

  doi = {10.1145/1103900.1103933},

  acmid = {1103933},

  publisher = {ACM},

  address = {New York, NY, USA},

 } 

 @book{burge1975recursive,

   title={Recursive Programming Techniques},

   author={Burge, William H.},

   year={1975},

   isbn = {0201144506},

   publisher={Addison-Wesley},

 }

 @book{paulson1994isabelle,

   author    = {Lawrence C. Paulson},

   title     = {Isabelle - A Generic Theorem Prover},

   publisher = {Springer-Verlag},

   series    = {Lecture Notes in Computer Science},

   volume    = {828},

   year      = {1994},

   isbn      = {3-540-58244-4},

   ee        = {http://dx.doi.org/10.1007/BFb0030541},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @phdthesis{neuper2001reactive,

   title={Reactive User-Guidance by an Autonomous Engine Doing High-School Math},

   author={Neuper, Walther},

   year={2001},

   school={Graz University of Technology}

 }

 @book{hammond2000research,

  editor = {Hammond, Kevin and Michelson, Greg},

  title = {Research Directions in Parallel Functional Programming},

  year = {2000},

  isbn = {1852330929},

  publisher = {Springer-Verlag},

  address = {London, UK, UK},

 }

 @article{hudak1989conception,

  author = {Hudak, Paul},

  title = {Conception, Evolution, and Application of Functional Programming Languages},

  journal = {ACM Comput. Surv.},

  issue_date = {Sep. 1989},

  volume = {21},

  number = {3},

  month = sep,

  year = {1989},

  issn = {0360-0300},

  pages = {359--411},

  numpages = {53},

  url = {http://doi.acm.org/10.1145/72551.72554},

  doi = {10.1145/72551.72554},

  acmid = {72554},

  publisher = {ACM},

  address = {New York, NY, USA},

 }

 @article{church1932set,

   title={A set of postulates for the foundation of logic},

   author={Church, Alonzo},

   journal={Annals of mathematics},

   volume={33},

   number={2},

   pages={346--366},

   year={1932}

 }

 @article{church1940formulation,

   author    = {Alonzo Church},

   title     = {A Formulation of the Simple Theory of Types},

   journal   = {Journal of Symbolic Logic},

   volume    = {5},

   number    = {2},

   year      = {1940},

   pages     = {56-68},

   ee        = {http://projecteuclid.org/euclid.jsl/1183387805},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{mccarthy1978history,

  author = {McCarthy, John},

  title = {History of LISP},

  journal = {SIGPLAN Not.},

  issue_date = {August 1978},

  volume = {13},

  number = {8},

  month = aug,

  year = {1978},

  issn = {0362-1340},

  pages = {217--223},

  numpages = {7},

  url = {http://doi.acm.org/10.1145/960118.808387},

  doi = {10.1145/960118.808387},

  acmid = {808387},

  publisher = {ACM},

  address = {New York, NY, USA},

 } 

 @article{backus1978can,

   author    = {John W. Backus},

   title     = {Can Programming Be Liberated From the von Neumann Style?

                A Functional Style and its Algebra of Programs},

   journal   = {Communications of the ACM},

   volume    = {21},

   number    = {8},

   year      = {1978},

   pages     = {613-641},

   ee        = {http://doi.acm.org/10.1145/359576.359579},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{milner1978theory,

   author    = {Robin Milner},

   title     = {A Theory of Type Polymorphism in Programming},

   journal   = {Journal of Computer and System Sciences},

   volume    = {17},

   number    = {3},

   year      = {1978},

   pages     = {348-375},

   ee        = {http://dx.doi.org/10.1016/0022-0000(78)90014-4},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @book{milner1997definition,

  author = {Milner, Robin and Tofte, Mads and Macqueen, David},

  title = {The  Definition of Standard ML},

  year = {1997},

  isbn = {0262631814},

  publisher = {MIT Press},

  address = {Cambridge, MA, USA},

 } 

 @article{jones2003haskell,

   author = {Simon {Peyton Jones} and others},

   title = {The {Haskell} 98 Language and Libraries: The Revised Report},

   journal = {Journal of Functional Programming},

   volume = 13,

   number = 1,

   pages = {0--255},

   month = {Jan},

   year = 2003,

   url = {http://www.haskell.org/definition/},

 }

 @online{haskell2013functional,

   title={Functional programming - HaskellWiki},

   url={http://www.haskell.org/haskellwiki/Functional_programming},

   year={2013}

 }

 @inproceedings{peyton1993imperative,

   author    = {Simon L. Peyton Jones and

                Philip Wadler},

   title     = {Imperative Functional Programming},

   booktitle = {POPL},

   year      = {1993},

   pages     = {71-84},

   ee        = {http://doi.acm.org/10.1145/158511.158524},

   crossref  = {DBLP:conf/popl/1993},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{achten1995ins,

   author    = {Peter Achten and

                Marinus J. Plasmeijer},

   title     = {The Ins and Outs of Clean I/O},

   journal   = {Journal of Functional Programming},

   volume    = {5},

   number    = {1},

   year      = {1995},

   pages     = {81-110},

   ee        = {http://dx.doi.org/10.1017/S0956796800001258},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{wadler1990linear,

   AUTHOR = {P. Wadler},

   TITLE = {Linear types can change the world!},

   BOOKTITLE = {{IFIP {TC} 2} Working Conference on Programming Concepts and Methods},

   WHERE = {{Sea of Galilee, Israel}},

   PUBLISHER = {North Holland},

   EDITOR = {M. Broy and C. Jones},

   PAGES = {347--359},

   YEAR = {1990}

 }

 @inproceedings{launchbury1993natural,

  author = {Launchbury, John},

  title = {A Natural Semantics for Lazy Evaluation},

  booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},

  series = {POPL '93},

  year = {1993},

  isbn = {0-89791-560-7},

  venue = {Charleston, South Carolina, USA},

  pages = {144--154},

  numpages = {11},

  url = {http://doi.acm.org/10.1145/158511.158618},

  doi = {10.1145/158511.158618},

  acmid = {158618},

  publisher = {ACM},

  address = {New York, NY, USA},

 }

 @phdthesis{lippmeier2009type,

   title={Type Inference and Optimisation for an Impure World},

   author={Lippmeier, Ben},

   year={2009},

   school={Australian National University}

 }

 @inproceedings{amdahl1967validity,

  author = {Amdahl, Gene M.},

  title = {Validity of the Single Processor Approach to Achieving Large Scale Computing Capabilities},

  booktitle = {Proceedings of the April 18-20, 1967, Spring Joint Computer Conference},

  series = {AFIPS '67 (Spring)},

  year = {1967},

  venue = {Atlantic City, New Jersey},

  pages = {483--485},

  numpages = {3},

  url = {http://doi.acm.org/10.1145/1465482.1465560},

  doi = {10.1145/1465482.1465560},

  acmid = {1465560},

  publisher = {ACM},

  address = {New York, NY, USA},

 }

 @article{gustafson1988reevaluating,

   author    = {John L. Gustafson},

   title     = {Reevaluating Amdahl's Law},

   journal   = {Communications of the ACM},

   volume    = {31},

   number    = {5},

   year      = {1988},

   pages     = {532-533},

   ee        = {http://doi.acm.org/10.1145/42411.42415},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{moler1986matrix,

   title={Matrix computation on distributed memory multiprocessors},

   author={Moler, Cleve},

   journal={Hypercube Multiprocessors},

   volume={86},

   pages={181--195},

   year={1986}

 }

 @article{geer2005chip,

   author    = {David Geer},

   title     = {Industry Trends: Chip Makers Turn to Multicore Processors},

   journal   = {IEEE Computer},

   volume    = {38},

   number    = {5},

   year      = {2005},

   pages     = {11-13},

   ee        = {http://doi.ieeecomputersociety.org/10.1109/MC.2005.160},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @book{culler1999parallel,

   author    = {David E. Culler and

                Jaswinder Pal Singh and

                Anoop Gupta},

   title     = {Parallel computer architecture - a hardware / software approach},

   publisher = {Morgan Kaufmann},

   year      = {1999},

   isbn      = {978-1-55860-343-1},

   pages     = {I-XXIX, 1-1024},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @book{hennessy2012computer,

   author    = {John L. Hennessy and

                David A. Patterson},

   title     = {Computer Architecture - A Quantitative Approach (5. ed.)},

   publisher = {Morgan Kaufmann},

   year      = {2012},

   isbn      = {978-0-12-383872-8},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{tullsen1995simultaneous,

  author = {Tullsen, Dean M. and Eggers, Susan J. and Levy, Henry M.},

  title = {Simultaneous Multithreading: Maximizing On-chip Parallelism},

  booktitle = {Proceedings of the 22nd Annual International Symposium on Computer Architecture},

  series = {ISCA '95},

  year = {1995},

  isbn = {0-89791-698-0},

  venue = {S. Margherita Ligure, Italy},

  pages = {392--403},

  numpages = {12},

  url = {http://doi.acm.org/10.1145/223982.224449},

  doi = {10.1145/223982.224449},

  acmid = {224449},

  publisher = {ACM},

  address = {New York, NY, USA},

 }

 @article{moore2008multicore,

   title={Multicore is bad news for supercomputers},

   author={Moore, Samuel K.},

   journal={Spectrum, IEEE},

   volume={45},

   number={11},

   pages={15},

   year={2008},

   publisher={IEEE},

   month={nov}

 }

 @inproceedings{li2007efficient,

  author = {Li, Tong and Baumberger, Dan and Koufaty, David A. and Hahn, Scott},

  title = {Efficient Operating System Scheduling for Performance-Asymmetric Multi-Core Architectures},

  booktitle = {Proceedings of the 2007 ACM/IEEE Conference on Supercomputing},

  series = {SC '07},

  year = {2007},

  isbn = {978-1-59593-764-3},

  venue = {Reno, Nevada},

  pages = {53:1--53:11},

  articleno = {53},

  numpages = {11},

  url = {http://doi.acm.org/10.1145/1362622.1362694},

  doi = {10.1145/1362622.1362694},

  acmid = {1362694},

  publisher = {ACM},

  address = {New York, NY, USA},

 }

 @article{henderson1986functional,

   author    = {Peter B. Henderson},

   title     = {Functional Programming, Formal Specification, and Rapid

                Prototyping},

   journal   = {IEEE Transactions on Software Engineering},

   volume    = {12},

   number    = {2},

   year      = {1986},

   pages     = {241-250},

   ee        = {http://doi.ieeecomputersociety.org/10.1109/TSE.1986.6312939},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{harris2007feedback,

  author = {Harris, Tim and Singh, Satnam},

  title = {Feedback Directed Implicit Parallelism},

  booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming},

  series = {ICFP '07},

  year = {2007},

  isbn = {978-1-59593-815-2},

  venue = {Freiburg, Germany},

  pages = {251--264},

  numpages = {14},

  url = {http://doi.acm.org/10.1145/1291151.1291192},

  doi = {10.1145/1291151.1291192},

  acmid = {1291192},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {functional programming, haskell, implicit parallelism},

 }

 @article{cantrill2008real,

   author    = {Bryan Cantrill and

                Jeff Bonwick},

   title     = {Real-World Concurrency},

   journal   = {ACM Queue},

   volume    = {6},

   number    = {5},

   year      = {2008},

   pages     = {16-25},

   ee        = {http://doi.acm.org/10.1145/1454456.1454462},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{thompson2005refactoring,

  author = {Thompson, Simon},

  title = {Refactoring Functional Programs},

  booktitle = {Proceedings of the 5th International Conference on Advanced Functional Programming},

  series = {AFP'04},

  year = {2005},

  isbn = {3-540-28540-7, 978-3-540-28540-3},

  venue = {Tartu, Estonia},

  pages = {331--357},

  numpages = {27},

  url = {http://dx.doi.org/10.1007/11546382_9},

  doi = {10.1007/11546382_9},

  acmid = {2162147},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 @inproceedings{hammer2007proposal,

  author = {Hammer, Matthew and Acar, Umut A. and Rajagopalan, Mohan and Ghuloum, Anwar},

  title = {A Proposal for Parallel Self-adjusting Computation},

  booktitle = {Proceedings of the 2007 Workshop on Declarative Aspects of Multicore Programming},

  series = {DAMP '07},

  year = {2007},

  isbn = {978-1-59593-690-5},

  venue = {Nice, France},

  pages = {3--9},

  numpages = {7},

  url = {http://doi.acm.org/10.1145/1248648.1248651},

  doi = {10.1145/1248648.1248651},

  acmid = {1248651},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {change propagation, dynamic dependency graphs, fork-join programs, parallel change propagation, parallelism, self-adjusting computation, series-parallel programs},

 }

 @inproceedings{nocker1991concurrent,

  author = {N\"{o}cker, Eric and Smesters, J. E. W. and van Eekelen, M. C. J. D. and Plasmeijer, M. J.},

  title = {Concurrent Clean},

  booktitle = {Proceedings on Parallel Architectures and Languages Europe: Volume II: Parallel Languages},

  series = {PARLE '91},

  year = {1991},

  isbn = {0-387-54152-7},

  venue = {Eindhoven, The Netherlands},

  pages = {202--219},

  numpages = {18},

  url = {http://dl.acm.org/citation.cfm?id=111634.111646},

  acmid = {111646},

  publisher = {Springer-Verlag New York, Inc.},

  address = {New York, NY, USA},

 }

 @inproceedings{marlow2009runtime,

  author = {Marlow, Simon and Peyton Jones, Simon and Singh, Satnam},

  title = {Runtime Support for Multicore Haskell},

  booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},

  series = {ICFP '09},

  year = {2009},

  isbn = {978-1-60558-332-7},

  venue = {Edinburgh, Scotland},

  pages = {65--78},

  numpages = {14},

  url = {http://doi.acm.org/10.1145/1596550.1596563},

  doi = {10.1145/1596550.1596563},

  acmid = {1596563},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {Haskell parallel runtime},

 }

 @article{nickolls2010gpu,

   author    = {John Nickolls and

                William J. Dally},

   title     = {The GPU Computing Era},

   journal   = {IEEE Micro},

   volume    = {30},

   number    = {2},

   year      = {2010},

   pages     = {56-69},

   ee        = {http://doi.ieeecomputersociety.org/10.1109/MM.2010.41},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{tarditi2006accelerator,

  author = {Tarditi, David and Puri, Sidd and Oglesby, Jose},

  title = {Accelerator: Using Data Parallelism to Program GPUs for General-purpose Uses},

  journal = {SIGOPS Oper. Syst. Rev.},

  issue_date = {December 2006},

  volume = {40},

  number = {5},

  month = {oct},

  year = {2006},

  issn = {0163-5980},

  pages = {325--335},

  numpages = {11},

  doi = {10.1145/1168917.1168898},

  publisher = {ACM},

 }

 @article{blelloch90compiling,

   author    = {Guy E. Blelloch and

                Gary Sabot},

   title     = {Compiling Collection-Oriented Languages onto Massively Parallel

                Computers},

   journal   = {Journal of Parallel and Distributed Computing},

   volume    = {8},

   number    = {2},

   year      = {1990},

   pages     = {119--134},

   ee        = {http://dx.doi.org/10.1016/0743-7315(90)90087-6},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{peytonjones2008harnessing,

  author = {Peyton Jones, Simon},

  title = {Harnessing the Multicores: Nested Data Parallelism in Haskell},

  booktitle = {Proceedings of the 6th Asian Symposium on Programming Languages and Systems},

  series = {APLAS '08},

  year = {2008},

  isbn = {978-3-540-89329-5},

  venue = {Bangalore, India},

  pages = {138--138},

  numpages = {1},

  url = {http://dx.doi.org/10.1007/978-3-540-89330-1_10},

  doi = {10.1007/978-3-540-89330-1_10},

  acmid = {1485356},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 @inproceedings{baker1977incremental,

  author = {Baker,Jr., Henry C. and Hewitt, Carl},

  title = {The Incremental Garbage Collection of Processes},

  booktitle = {Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages},

  year = {1977},

  pages = {55--59},

  numpages = {5},

  url = {http://doi.acm.org/10.1145/800228.806932},

  doi = {10.1145/800228.806932},

  acmid = {806932},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {Eager evaluation, Garbage collection, Lazy evaluation, Multiprocessing systems, Processor scheduling},

 }

 @article{halstead1985multilisp,

   author    = {Robert H. Halstead Jr.},

   title     = {Multilisp: A Language for Concurrent Symbolic Computation},

   journal   = {ACM Transactions on Programming Languages and Systems},

   volume    = {7},

   number    = {4},

   year      = {1985},

   pages     = {501-538},

   ee        = {http://doi.acm.org/10.1145/4472.4478},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{matthews2010efficient,

  author = {Matthews, David C. J. and Wenzel, Makarius},

  title = {Efficient Parallel Programming in Poly/ML and Isabelle/ML},

  booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming},

  series = {DAMP '10},

  year = {2010},

  isbn = {978-1-60558-859-9},

  venue = {Madrid, Spain},

  pages = {53--62},

  numpages = {10},

  url = {http://doi.acm.org/10.1145/1708046.1708058},

  doi = {10.1145/1708046.1708058},

  acmid = {1708058},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {data parallelism, isabelle, parallel standard ml, poly/ml, theorem proving applications},

 }

 @article{wegner1990concepts,

   author    = {Peter Wegner},

   title     = {Concepts and paradigms of object-oriented programming},

   journal   = {OOPS Messenger},

   volume    = {1},

   number    = {1},

   year      = {1990},

   pages     = {7-87},

   ee        = {http://doi.acm.org/10.1145/382192.383004},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{shavit1997software,

   title={Software transactional memory},

   author={Shavit, Nir and Touitou, Dan},

   journal={Distributed Computing},

   volume={10},

   number={2},

   pages={99--116},

   year={1997},

   publisher={Springer-Verlag}

 }

 @article{herlihy1990linearizability,

  author = {Herlihy, Maurice P. and Wing, Jeannette M.},

  title = {Linearizability: A Correctness Condition for Concurrent Objects},

  journal = {ACM Trans. Program. Lang. Syst.},

  issue_date = {July 1990},

  volume = {12},

  number = {3},

  month = jul,

  year = {1990},

  issn = {0164-0925},

  pages = {463--492},

  numpages = {30},

  url = {http://doi.acm.org/10.1145/78969.78972},

  doi = {10.1145/78969.78972},

  acmid = {78972},

  publisher = {ACM},

  address = {New York, NY, USA},

 } 

 @inproceedings{ramadan2009committing,

  author = {Ramadan, Hany E. and Roy, Indrajit and Herlihy, Maurice and Witchel, Emmett},

  title = {Committing Conflicting Transactions in an STM},

  booktitle = {Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},

  series = {PPoPP '09},

  year = {2009},

  isbn = {978-1-60558-397-6},

  venue = {Raleigh, NC, USA},

  pages = {163--172},

  numpages = {10},

  url = {http://doi.acm.org/10.1145/1504176.1504201},

  doi = {10.1145/1504176.1504201},

  acmid = {1504201},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {concurrency control, dependence-aware, serializability, transactional memory},

 }

 @inproceedings{herlihy2003software,

  author = {Herlihy, Maurice and Luchangco, Victor and Moir, Mark and Scherer,III, William N.},

  title = {Software Transactional Memory for Dynamic-sized Data Structures},

  booktitle = {Proceedings of the Twenty-second Annual Symposium on Principles of Distributed Computing},

  series = {PODC '03},

  year = {2003},

  isbn = {1-58113-708-7},

  venue = {Boston, Massachusetts},

  pages = {92--101},

  numpages = {10},

  url = {http://doi.acm.org/10.1145/872035.872048},

  doi = {10.1145/872035.872048},

  acmid = {872048},

  publisher = {ACM},

  address = {New York, NY, USA},

 }

 @patent{zhang2010software,

   title={Software Transaction Commit Order and Conflict Management},

   author={Zhang, Lingli and Grover, Vinod K. and Magruder, Michael M. and Detlefs, David and Duffy, John J. and Graefe, Goetz},

   url={http://www.google.co.in/patents/US7711678},

   year={2010},

   month={5},

   number={US 7711678}

 }

 @techreport{ennals2006software,

   title={Software transactional memory should not be obstruction-free},

   author={Ennals, Robert},

   year={2006},

   institution={Technical Report IRC-TR-06-052, Intel Research Cambridge Tech Report}

 }

 @techreport{ennals2005efficient,

   author	= {Ennals, Robert},

   title		= {Efficient Software Transactional Memory},

   institution	= {Intel Research Cambridge Tech Report},

   number	= {IRC-TR-05-051},

   pdf		= {http://www.cs.wisc.edu/trans-memory/misc-papers/051_Rob_Ennals.pdf},

   year		= {2005},

   month		= {Jan}

 }

 @inproceedings{saha2006mcrt,

  author = {Saha, Bratin and Adl-Tabatabai, Ali-Reza and Hudson, Richard L. and Minh, Chi Cao and Hertzberg, Benjamin},

  title = {McRT-STM: A High Performance Software Transactional Memory System for a Multi-Core Runtime},

  booktitle = {Proceedings of the Eleventh ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},

  series = {PPoPP '06},

  year = {2006},

  isbn = {1-59593-189-9},

  pages = {187--197},

  numpages = {11},

  doi = {10.1145/1122971.1123001},

  publisher = {ACM}

 }

 @inproceedings{harris2005composable,

  author = {Harris, Tim and Marlow, Simon and Peyton-Jones, Simon and Herlihy, Maurice},

  title = {Composable Memory Transactions},

  booktitle = {Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},

  series = {PPoPP '05},

  year = {2005},

  isbn = {1-59593-080-9},

  venue = {Chicago, IL, USA},

  pages = {48--60},

  numpages = {13},

  url = {http://doi.acm.org/10.1145/1065944.1065952},

  doi = {10.1145/1065944.1065952},

  acmid = {1065952},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {locks, non-blocking algorithms, transactions},

 }

 @inproceedings{hewitt1973universal,

  author = {Hewitt, Carl and Bishop, Peter and Steiger, Richard},

  title = {A Universal Modular ACTOR Formalism for Artificial Intelligence},

  booktitle = {Proceedings of the 3rd International Joint Conference on Artificial Intelligence},

  series = {IJCAI'73},

  year = {1973},

  venue = {Stanford, USA},

  pages = {235--245},

  numpages = {11},

  url = {http://dl.acm.org/citation.cfm?id=1624775.1624804},

  acmid = {1624804},

  publisher = {Morgan Kaufmann Publishers Inc.},

  address = {San Francisco, CA, USA},

 }

 @article{hewitt1977viewing,

   author    = {Carl Hewitt},

   title     = {Viewing Control Structures as Patterns of Passing Messages},

   journal   = {Artificial Intelligence},

   volume    = {8},

   number    = {3},

   year      = {1977},

   pages     = {323--364},

   ee        = {http://dx.doi.org/10.1016/0004-3702(77)90033-9},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{agha1985actors,

   author    = {Gul A. Agha},

   title     = {ACTORS - a model of concurrent computation in distributed

                systems},

   publisher = {MIT Press},

   series    = {MIT Press series in artificial intelligence},

   year      = {1990},

   isbn      = {978-0-262-01092-4},

   pages     = {I-IX, 1-144},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{agha1997foundation,

   author    = {Gul A. Agha and

                Ian A. Mason and

                Scott F. Smith and

                Carolyn L. Talcott},

   title     = {A Foundation for Actor Computation},

   journal   = {Journal of Functional Programming},

   volume    = {7},

   number    = {1},

   year      = {1997},

   pages     = {1--72},

   ee        = {http://journals.cambridge.org/action/displayAbstract?aid=44065},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @misc{thurauakka,

   title={Akka framework},

   author={Thurau, Martin},

   year={2012},

   howpublished={Paper for Seminar Software Systems Engineering, Universität zu Lübeck},

   url={http://media.itm.uni-luebeck.de/teaching/ws2012/sem-sse/martin-thurau-akka.io.pdf}

 }

 @inproceedings{karmani2009actor,

  author = {Karmani, Rajesh K. and Shali, Amin and Agha, Gul A.},

  title = {Actor Frameworks for the JVM Platform: A Comparative Analysis},

  booktitle = {Proceedings of the 7th International Conference on Principles and Practice of Programming in Java},

  series = {PPPJ '09},

  year = {2009},

  isbn = {978-1-60558-598-7},

  venue = {Calgary, Alberta, Canada},

  pages = {11--20},

  numpages = {10},

  url = {http://doi.acm.org/10.1145/1596655.1596658},

  doi = {10.1145/1596655.1596658},

  acmid = {1596658},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {JVM, Java, abstractions, actors, comparison, frameworks, libraries, performance, semantics},

 }

 @article{fuggetta1998understanding,

   author    = {Alfonso Fuggetta and

                Gian Pietro Picco and

                Giovanni Vigna},

   title     = {Understanding Code Mobility},

   journal   = {IEEE Transactions on Software Engineering},

   volume    = {24},

   number    = {5},

   year      = {1998},

   pages     = {342-361},

   ee        = {http://doi.ieeecomputersociety.org/10.1109/32.685258},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{panwar1994methodology,

   author    = {Rajendra Panwar and

                Gul A. Agha},

   title     = {A Methodology for Programming Scalable Architectures},

   journal   = {Journal of Parallel and Distributed Computing},

   volume    = {22},

   number    = {3},

   year      = {1994},

   pages     = {479-487},

   ee        = {http://dx.doi.org/10.1006/jpdc.1994.1105},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @techreport{odersky2004overview,

   title={An overview of the Scala programming language},

   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},

   year={2006},

   institution={École Polytechnique Fédérale de Lausanne},

   address={1015 Lausanne, Switzerland},

   number={LAMP-REPORT-2006-001},

   note={2nd edition}

 }

 @incollection{haller2006event,

   title={Event-based programming without inversion of control},

   author={Haller, Philipp and Odersky, Martin},

   booktitle={Modular Programming Languages},

   pages={4--22},

   year={2006},

   publisher={Springer-Verlag}

 }

 @article{haller2009scala,

   title={Scala actors: Unifying thread-based and event-based programming},

   author={Haller, Philipp and Odersky, Martin},

   journal={Theoretical Computer Science},

   volume={410},

   number={2},

   pages={202--220},

   year={2009},

   publisher={Elsevier}

 }

 @online {akka2014futures,

   title={Futures (Scala) -- Akka Documentation},

   url={http://doc.akka.io/docs/akka/current/scala/futures.html},

   urldate={2014-06-05},

   year={2014}

 }

 @online {scala2014migration,

   title={The Scala Actors Migration Guide - Scala Documentation},

   author={Jovanovic, Vojin and Haller, Philipp},

   url={http://docs.scala-lang.org/overviews/core/actors-migration-guide.html},

   year={2014}

 }

 @inproceedings{tasharofi2013scala,

  author = {Tasharofi, Samira and Dinges, Peter and Johnson, Ralph E.},

  title = {Why Do Scala Developers Mix the Actor Model with Other Concurrency Models?},

  booktitle = {Proceedings of the 27th European Conference on Object-Oriented Programming},

  series = {ECOOP'13},

  year = {2013},

  isbn = {978-3-642-39037-1},

  venue = {Montpellier, France},

  pages = {302--326},

  numpages = {25},

  url = {http://dx.doi.org/10.1007/978-3-642-39038-8_13},

  doi = {10.1007/978-3-642-39038-8_13},

  acmid = {2525001},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 @article{hoare1978communicating,

   author    = {C. A. R. Hoare},

   title     = {Communicating Sequential Processes},

   journal   = {Communications of the ACM},

   volume    = {21},

   number    = {8},

   year      = {1978},

   pages     = {666-677},

   ee        = {http://doi.acm.org/10.1145/359576.359585},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @book{INMOS84occam,

   author = {{INMOS, Ltd.}},

   year = {1984},

   address = {Englewood Cliffs},

   publisher = {Prentice Hall},

   title = {The occam programming manual}

 }

 @inproceedings{dorward1997programming,

  author = {Dorward, Sean and Pike, Rob and Winterbottom, Phil},

  title = {Programming in Limbo},

  booktitle = {Proceedings of the 42Nd IEEE International Computer Conference},

  series = {COMPCON '97},

  year = {1997},

  isbn = {0-8186-7804-6},

  pages = {245--},

  url = {http://dl.acm.org/citation.cfm?id=792770.793719},

  acmid = {793719},

  publisher = {IEEE Computer Society},

  address = {Washington, DC, USA},

  keywords = {programming languages, modules, graphics},

 }

 @inproceedings{pike2012go,

   author    = {Rob Pike},

   title     = {Go at Google},

   booktitle = {Proceedings of the Conference on Systems, Programming, and Applications: Software

                for Humanity},

   year      = {2012},

   pages     = {5-6},

   ee        = {http://doi.acm.org/10.1145/2384716.2384720},

   bibsource = {DBLP, http://dblp.uni-trier.de},

   venue     = {Tucson, AZ, USA},

   editor    = {Gary T. Leavens}

 }

 @inproceedings{brown2012paraforming,

  author = {Brown, Christopher and Loidl, Hans-Wolfgang and Hammond, Kevin},

  title = {ParaForming: Forming Parallel Haskell Programs Using Novel Refactoring Techniques},

  booktitle = {Proceedings of the 12th International Conference on Trends in Functional Programming},

  series = {TFP'11},

  year = {2012},

  isbn = {978-3-642-32036-1},

  venue = {Madrid, Spain},

  pages = {82--97},

  numpages = {16},

  url = {http://dx.doi.org/10.1007/978-3-642-32037-8_6},

  doi = {10.1007/978-3-642-32037-8_6},

  acmid = {2362972},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 @article{kennedy1991interactive,

   author    = {Ken Kennedy and

                Kathryn S. McKinley and

                Chau-Wen Tseng},

   title     = {Interactive Parallel Programming using the ParaScope Editor},

   journal   = {IEEE Transactions on Parallel and Distributed Systems},

   volume    = {2},

   number    = {3},

   year      = {1991},

   pages     = {329-341},

   ee        = {http://doi.ieeecomputersociety.org/10.1109/71.86108},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{wloka2009refactoring,

  author = {Wloka, Jan and Sridharan, Manu and Tip, Frank},

  title = {Refactoring for Reentrancy},

  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},

  series = {ESEC/FSE '09},

  year = {2009},

  isbn = {978-1-60558-001-2},

  venue = {Amsterdam, The Netherlands},

  pages = {173--182},

  numpages = {10},

  url = {http://doi.acm.org/10.1145/1595696.1595723},

  doi = {10.1145/1595696.1595723},

  acmid = {1595723},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {program transformation, reentrant code, refactoring},

 }

 @article{dig2011refactoring,

   author    = {Danny Dig},

   title     = {A Refactoring Approach to Parallelism},

   journal   = {IEEE Software},

   volume    = {28},

   number    = {1},

   year      = {2011},

   pages     = {17-22},

   ee        = {http://doi.ieeecomputersociety.org/10.1109/MS.2011.1},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{brown2013cost,

   author    = {Christopher Brown and

                Marco Danelutto and

                Kevin Hammond and

                Peter Kilpatrick and

                Archibald Elliott},

   title     = {Cost-Directed Refactoring for Parallel Erlang Programs},

   journal   = {International Journal of Parallel Programming},

   volume    = {42},

   number    = {4},

   year      = {2014},

   pages     = {564-582},

   ee        = {http://dx.doi.org/10.1007/s10766-013-0266-5},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{brown2012language,

  author = {Brown, Christopher and Hammond, Kevin and Danelutto, Marco and Kilpatrick, Peter},

  title = {A Language-Independent Parallel Refactoring Framework},

  booktitle = {Proceedings of the Fifth Workshop on Refactoring Tools},

  series = {WRT '12},

  year = {2012},

  isbn = {978-1-4503-1500-5},

  venue = {Rapperswil, Switzerland},

  pages = {54--58},

  numpages = {5},

  url = {http://doi.acm.org/10.1145/2328876.2328884},

  doi = {10.1145/2328876.2328884},

  acmid = {2328884},

  publisher = {ACM},

  address = {New York, NY, USA},

  keywords = {C/C++, Erlang, ParaPhrase, concurrency, parallelism, patterns, refactoring, skeletons},

 }

 @incollection{hammond2013paraphrase,

 	year={2013},

 	isbn={978-3-642-35886-9},

 	booktitle={Formal Methods for Components and Objects},

 	volume={7542},

 	series={Lecture Notes in Computer Science},

 	editor={Beckert, Bernhard and Damiani, Ferruccio and de Boer, FrankS. and Bonsangue, MarcelloM.},

 	doi={10.1007/978-3-642-35887-6_12},

 	title={The ParaPhrase Project: Parallel Patterns for Adaptive Heterogeneous Multicore Systems},

 	url={http://dx.doi.org/10.1007/978-3-642-35887-6_12},

 	publisher={Springer-Verlag},

 	address={Berlin, Heidelberg},

 	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},

 	pages={218-236},

 	language={English}

 }

 @inproceedings{li2006comparative,

  author = {Li, Huiqing and Thompson, Simon},

  title = {Comparative Study of Refactoring Haskell and Erlang Programs},

  booktitle = {Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation},

  series = {SCAM '06},

  year = {2006},

  isbn = {0-7695-2353-6},

  pages = {197--206},

  numpages = {10},

  url = {http://dx.doi.org/10.1109/SCAM.2006.8},

  doi = {10.1109/SCAM.2006.8},

  acmid = {1174113},

  publisher = {IEEE Computer Society},

  address = {Washington, DC, USA},

 }

 @article{hindley1969principal,

     author = {Hindley, R.},

     doi = {10.2307/1995158},

     issn = {00029947},

     journal = {Transactions of the American Mathematical Society},

     pages = {29--60},

     publisher = {American Mathematical Society},

     title = {{The Principal Type-Scheme of an Object in Combinatory Logic}},

     volume = {146},

     year = {1969}

 }

 @inproceedings{milner1975logic,

   title={{A Logic for Computable Functions with Reflexive and Polymorphic Types}},

   author={Milner, Robin and Morris, Lockwood and Newey, Malcolm},

   year={1975},

   booktitle = {Proceedings of the Conference on Proving and Improving Programs}

 }

 @phdthesis{damas1984type,

   title={Type assignment in programming languages.},

   author={Damas, Luis Manuel Martins},

   year={1984},

   school={University of Edinburgh}

 }

 @article{paulson1989foundation,

   author    = {Lawrence C. Paulson},

   title     = {The Foundation of a Generic Theorem Prover},

   journal   = {Journal of Automated Reasoning},

   volume    = {5},

   number    = {3},

   year      = {1989},

   pages     = {363-397},

   ee        = {http://dx.doi.org/10.1007/BF00248324},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{weeks2006whole,

  author = {Weeks, Stephen},

  title = {Whole-program Compilation in MLton},

  booktitle = {Proceedings of the 2006 Workshop on ML},

  series = {ML '06},

  year = {2006},

  isbn = {1-59593-483-9},

  venue = {Portland, Oregon, USA},

  pages = {1--1},

  numpages = {1},

  url = {http://doi.acm.org/10.1145/1159876.1159877},

  doi = {10.1145/1159876.1159877},

  acmid = {1159877},

  publisher = {ACM},

  address = {New York, NY, USA},

 }

 @online{smlnj2013standard,

   url={http://www.smlnj.org/},

   title={Standard ML of New Jersey},

   author={SML/NJ Fellowship, The},

   urldate={2014-05-15}

 }

 @online{romanenko2014moscow,

   url={http://mosml.org/},

   title={Moscow ML},

   year={2014-05-15}

 }

 @online{matthews2014documentation,

   url={http://polyml.org/Doc.html},

   title={Documentation},

   author={Matthews, David C. J.},

   year={2014-05-15}

 }

 @techreport{matthews1995papers,

   author =	 {Matthews, David C. J.},

   title = 	 {{Papers on Poly/ML}},

   year = 	 {1989},

   month = 	 {feb},

   institution =  {Computer Laboratory, University of Cambridge}

 }

 @techreport{matthews1991distributed,

   title={A Distributed Concurrent Implementation of Standard ML},

   author={Matthews, David C. J.},

   year={1991},

   institution={LFCS, Department of Computer Science, University of Edinburgh}

 }

 @inproceedings{reppy1993concurrent,

  author = {Reppy, John H.},

  title = {Concurrent ML: Design, Application and Semantics},

  booktitle = {Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992},

  venue={McMaster University, Hamilton, Ontario, Canada},

  year = {1993},

  isbn = {3-540-56883-2},

  pages = {165--198},

  numpages = {34},

  publisher = {Springer-Verlag}

 }

 @manual{wenzel2013isar,

   title={The Isabelle/Isar Reference Manual},

   author={Wenzel, Makarius and others},

   year={2013},

   url={http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf}

 }

 @incollection{wenzel1999isar,

   volume={1690},

   series={Lecture Notes in Computer Science},

   editor={Bertot, Yves and Dowek, Gilles and Théry, Laurent and Hirschowitz, André and Paulin, Christine},

   doi={10.1007/3-540-48256-3_12},

   title={Isar — A Generic Interpretative Approach to Readable Formal Proof Documents},

   author={Wenzel, Makarius},

   booktitle={Theorem Proving in Higher Order Logics},

   pages={167--183},

   year={1999},

   publisher={Springer-Verlag},

   address={Berlin, Heidelberg},

   isbn={978-3-540-66463-5}

 }

 @inproceedings{wenzel2014uipide,

   title={Asynchronous User Interaction and Tool Integration in Isabelle/PIDE},

   author={Wenzel, Makarius},

   year={2014},

     month            = {jul},

     booktitle={Proceedings of the 5th Int.\ Conference on Interactive Theorem Proving},

     venue={Vienna, Austria},

     editor           = {Klein, G and Gamboa, R}

 }

 @inproceedings{matichuk2014isabelle,

     author = {Matichuk, Daniel and Wenzel, Makarius and Murray, Toby},

     month            = {jul},

     year             = {2014},

     title            = {An Isabelle Proof Method Language},

     booktitle={Proceedings of the 5th Int.\ Conference on Interactive Theorem Proving},

     publisher        = {Springer-Verlag},

     venue={Vienna, Austria},

     editor           = {Klein, G and Gamboa, R}

 }

 @article{wenzel2012asynchronous,

   author    = {Makarius Wenzel},

   title     = {Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit},

   journal   = {Electronic Notes in Theoretical Computer Science},

   volume    = {285},

   year      = {2012},

   pages     = {101--114}

 }

 @manual{wenzel2013isabelle,

   title={The Isabelle System Manual},

   author={Wenzel, Makarius and Berghofer, Stefan},

   year={2013},

   url={http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/system.pdf}

 }

 @inproceedings{wenzel2011isabelle,

  author = {Wenzel, Makarius},

  title = {Isabelle As Document-Oriented Proof Assistant},

  booktitle = {Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics},

  series = {MKM'11},

  year = {2011},

  isbn = {978-3-642-22672-4},

  venue = {Bertinoro, Italy},

  pages = {244--259},

  numpages = {16},

  url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},

  acmid = {2032732},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 @inproceedings{wenzel2012isabelle,

  author = {Wenzel, Makarius},

  title = {Isabelle/jEdit: A Prover IDE Within the PIDE Framework},

  booktitle = {Proceedings of the 11th International Conference on Intelligent Computer Mathematics},

  series = {CICM'12},

  year = {2012},

  isbn = {978-3-642-31373-8},

  venue = {Bremen, Germany},

  pages = {468--471},

  numpages = {4},

  url = {http://dx.doi.org/10.1007/978-3-642-31374-5_38},

  doi = {10.1007/978-3-642-31374-5_38},

  acmid = {2352851},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 @manual{wenzel2013jedit,

   title={Isabelle/jEdit},

   author={Wenzel, Makarius},

   year={2013},

   url={http://isabelle.in.tum.de/dist/doc/jedit.pdf}

 }

 @book{chlipala2011certified,

  author = {Chlipala, Adam},

  title = {Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant},

  year = {2013},

  isbn = {0262026651, 9780262026659},

  publisher = {The MIT Press},

 } 

 @book{nipkow2002isabelle,

  author = {Nipkow, Tobias and Wenzel, Makarius and Paulson, Lawrence C.},

  title = {Isabelle/HOL: A Proof Assistant for Higher-order Logic},

  year = {2013},

  month = {12},

  isbn = {3-540-43376-7},

  publisher = {Springer-Verlag}

 }

 @manual{wenzel2013impl,

   title={The Isabelle/Isar Implementation},

   author={Wenzel, Makarius},

   year={2013},

   note={With contributions by Florian Haftmann and Larry Paulson},

   url={http://isabelle.in.tum.de/doc/implementation.pdf}

 }

 @book{van1979checking,

    title = {Checking Landau's ``Grundlagen'' in the Automath system},

    author = {van Benthem Jutting, L. S.},

    publisher = {Mathematisch Centrum},

    address = {Eindhoven},

    year = {1979}

 }

 @article{landin1966next,

   author    = {Peter J. Landin},

   title     = {The next 700 programming languages},

   journal   = {Communications of the ACM},

   volume    = {9},

   number    = {3},

   year      = {1966},

   pages     = {157--166}

 }

 @inproceedings{paulson1988isabelle,

  author = {Paulson, Lawrence C.},

  title = {Isabelle: The Next Seven Hundred Theorem Provers},

  booktitle = {Proceedings of the 9th International Conference on Automated Deduction},

  year = {1988},

  isbn = {3-540-19343-X},

  pages = {772--773},

  numpages = {2},

  url = {http://dl.acm.org/citation.cfm?id=648228.751990},

  acmid = {751990},

  publisher = {Springer-Verlag},

  address = {London, UK, UK},

 }

 @article{gentzen1964investigations,

   title={Investigations into logical deduction},

   author={Gentzen, Gerhard},

   journal={American philosophical quarterly},

   volume={1},

   number={4},

   pages={288--306},

   year={1964},

   publisher={JSTOR}

 }

 @article{coquand1988calculus,

   author    = {Thierry Coquand and

                G{\'e}rard P. Huet},

   title     = {The Calculus of Constructions},

   journal   = {Information and Computation},

   volume    = {76},

   number    = {2/3},

   year      = {1988},

   pages     = {95-120},

   ee        = {http://dx.doi.org/10.1016/0890-5401(88)90005-3},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @article{fitzgerald2008vdmtools,

   author    = {John S. Fitzgerald and

                Peter Gorm Larsen and

                Shin Sahara},

   title     = {VDMTools: advances in support for formal modeling in VDM},

   journal   = {SIGPLAN Notices},

   volume    = {43},

   number    = {2},

   year      = {2008},

   pages     = {3-11},

   ee        = {http://doi.acm.org/10.1145/1361213.1361214},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @incollection{fitzgerald2008vienna,

 	title = {Vienna Development Method},

 	author = {Fitzgerald, John S. and Larsen, Peter Gorm and Verhoef, Marcel},

 	publisher = {John Wiley \& Sons, Inc.},

 	isbn = {9780470050118},

 	url = {http://dx.doi.org/10.1002/9780470050118.ecse447},

 	doi = {10.1002/9780470050118.ecse447},

 	booktitle = {Wiley Encyclopedia of Computer Science and Engineering},

 	year = {2007}

 }

 @book{bjorner2006software,

   title={Software Engineering},

   author={Bj{\o}rner, Dines},

   volume={1,2,3},

   year={2006},

   series={Texts in Theoretical Computer Science},

   publisher={Springer-Verlag}

 }

 @article{back2010structured,

   author    = {Ralph-Johan Back},

   title     = {Structured derivations: a unified proof style for teaching mathematics},

   journal   = {Formal Aspects of Computing},

   volume    = {22},

   number    = {5},

   year      = {2010},

   pages     = {629--661}

 }

 @article{wenzel2007generic,

   title={Isabelle/Isar -- a generic framework for human-readable proof documents},

   author={Wenzel, Makarius},

   journal={From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec},

   volume={10},

   number={23},

   pages={277--298},

   year={2007}

 }

 @inproceedings{neuper2012automated,

   author    = {Walther Neuper},

   title     = {Automated Generation of User Guidance by Combining Computation

                and Deduction},

   editor    = {Pedro Quaresma and

                Ralph-Johan Back},

   booktitle = {Proceedings of the First Workshop on CTP Components for Educational

                Software (THedu'11)},

   year      = {2011},

   pages     = {82--101},

   series    = {EPTCS},

   volume    = {79},

   venue     = {Wroclaw, Poland},

   month     = {7}

 }

 @article{daroczy2013error,

   title={Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},

   author={Dar{\'o}czy, Gabriella and Neuper, Walther},

   journal={Electronic Journal of Mathematics \& Technology},

   volume={7},

   number={2},

   year={2013}

 }

 @mastersthesis{kienleitner2012towards,

   title={Towards ``NextStep Userguidance'' in a Mechanized Math Assistant},

   author={Kienleitner, Markus},

   school={Graz University of Technology},

   year={2012},

   type={Bachelor's thesis}

 }

 @inproceedings{wenzel2009parallel,

 	author = {Makarius Wenzel},

 	title = {{Parallel Proof Checking in {Isabelle/Isar}}},

 	booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)},

 	year = {2009},

 	editor = {Dos Reis, G and L Th\'ery},

 	publisher = {ACM Digital Library}

 }

 @techreport{buchberger1984mathematik,

   author={Buchberger, Bruno},

   title={Mathematik für Informatiker II (Problemlösestrategien und Algorithmentypen)},

   institution={RISC-Linz},

   type={Lecture notes},

   number={CAMP-Publ.-No. 84-4.0},

   year={1984}

 }

 @mastersthesis{lehnfeld2011verbindung,

   title={Verbindung von 'Computation' und 'Deduction' im \isac{}-System},

   author={Lehnfeld, Mathias},

   school={Technische Universität Wien},

   year={2011},

   type={Bachelor's project report}

 }

 @phdthesis{krauss2009automating,

   author    = {Alexander Krauss},

   title     = {Automating recursive definitions and termination proofs

                in higher-order logic},

   year      = {2009},

   pages     = {1-127},

   school    = {Technische Universität München},

   ee        = {http://mediatum2.ub.tum.de/doc/681651/document.pdf},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @mastersthesis{rocnik2012interactive,

   author={Jan Rocnik},

   title={Interactive Course Material for Signal Processing based on Isabelle/\isac{}},

   type={Bachelor's thesis},

   year={2012},

   url={http://www.ist.tugraz.at/projects/isac/publ/jrocnik_bakk.pdf},

   school={Graz University of Technology}

 }

 @inproceedings{haftmann2010code,

  author = {Haftmann, Florian and Nipkow, Tobias},

  title = {Code Generation via Higher-order Rewrite Systems},

  booktitle = {Proceedings of the 10th International Conference on Functional and Logic Programming},

  series = {FLOPS'10},

  year = {2010},

  isbn = {3-642-12250-7, 978-3-642-12250-7},

  venue = {Sendai, Japan},

  pages = {103--117},

  numpages = {15},

  url = {http://dx.doi.org/10.1007/978-3-642-12251-4_9},

  doi = {10.1007/978-3-642-12251-4_9},

  acmid = {2175441},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 @book{charniak2014artificial,

   author    = {Charniak, Eugene and Riesbeck, Christopher K. and McDermott, Drew V. and Meehan, James R.},

   title     = {Artificial Intelligence Programming},

   edition   = {2},

   isbn      = {0898596092},

   year      = {1987},

   publisher = {Psychology Press}

 }

 @inproceedings{aspinall2000proof,

  author = {Aspinall, David},

  title = {Proof General: A Generic Tool for Proof Development},

  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},

  series = {TACAS '00},

  year = {2000},

  isbn = {3-540-67282-6},

  pages = {38--42},

  numpages = {5},

  url = {http://dl.acm.org/citation.cfm?id=646484.691773},

  acmid = {691773},

  publisher = {Springer-Verlag},

  address = {London, UK, UK},

 }

 @book{simon1965shape,

     address = {New York},

     author = {Simon, Herbert A.},

     publisher = {Harper \& Row},

     title = {{The Shape of Automation for Men and Management}},

     year = {1965}

 }

 @book{gordon1993introduction,

   title={Introduction to HOL: A theorem proving environment for higher-order logic},

   author={Michael J. C. Gordon and Melham, Tom F.},

   year={1993},

   publisher={Cambridge University Press},

   isbn={0521441897}

 }

 @online{harrison2014hol,

   author={Harrison, John},

   title={HOL Light},

   urldate={2014-05-26},

   url={http://www.cl.cam.ac.uk/~jrh13/hol-light/}

 }

 @article{appel1977solution,

   title={The solution of the four-color-map problem},

   author={Appel, Kenneth and Haken, Wolfgang},

   journal={Scientific American},

   volume={237},

   pages={108--121},

   year={1977}

 }

 @incollection{hales2011historical,

 	year={2011},

 	isbn={978-1-4614-1128-4},

 	booktitle={The Kepler Conjecture},

 	editor={Lagarias, Jeffrey C.},

 	doi={10.1007/978-1-4614-1129-1_3},

 	title={Historical Overview of the Kepler Conjecture},

 	url={http://dx.doi.org/10.1007/978-1-4614-1129-1_3},

 	publisher={Springer New York},

 	author={Hales, Thomas C.},

 	pages={65-82},

 	language={English}

 }

 @techreport{sharangpani1994statistical,

   title={Statistical Analysis of Floating Point Flaw in the Pentium Processor},

   author={Sharangpani, H. P. and Barton, M. L.},

   institution={Intel Corporation},

   year={1994}

 }

 @online{intel1997intel,

   year={1997},

   title={Intel® Pentium® Processor - Invalid Instruction Erratum Overview},

   urldate={2014-05-26},

   url={http://www.intel.com/support/processors/pentium/ppiie/index.htm}

 }

 @article{brandt2007theorem,

   title={Theorem Proving in Higher Order Logics},

   author={Brandt, Klaus Schneider Jens},

   year={2007},

   publisher={Springer-Verlag}

 }

 @online{isabelle2013news,

   title={isabelle.in.tum.de/dist/Isabelle2013-2/NEWS},

   url={http://isabelle.in.tum.de/dist/Isabelle2013-2/NEWS},

   urldate={2014-05-27},

   year=2013

 }

 @online{isac2014knowledge,

   title={www.ist.tugraz.at/projects/isac/www/kbase/thy/index\_thy.html},

   url={http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html},

   urldate={2014-06-01}

 }

 @online{isac2014pbl,

   title={www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html},

   url={http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html},

   urldate={2014-06-01}

 }

 @online{isac2014met,

   title={www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html},

   url={http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html},

   urldate={2014-06-01}

 }

 @manual{krauss2013defining,

   title={Defining recursive functions in Isabelle/HOL},

   author={Krauss, Alexander},

   year={2013},

   url={http://isabelle.in.tum.de/doc/functions.pdf}

 }

 @online{google2012flyspeck,

   title={FlyspeckFactSheet},

   url={https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet},

   urldate={2014-06-01},

   year={2012}

 }

 @online{austriaforum2014zemanek,

   title={Zemanek, Heinz | Austria-Forum > Biographien},

   url={http://austria-forum.org/af/Wissenssammlungen/Biographien/Zemanek,_Heinz},

   urldate={2014-06-02}

 }

 @article{gonthier2008formal,

   title={Formal Proof --- The Four Colour Theorem},

   author={Gonthier, Georges},

   journal={Notices of the AMS},

   volume={55},

   number={11},

   pages={1382--1393},

   year={2008}

 }

 @online{pipermail2014clisa,

   title={The Cl-isabelle-users Archives},

   url={https://lists.cam.ac.uk/pipermail/cl-isabelle-users/},

   urldate={2014-06-05},

   year={2014}

 }

 @online{tum2013team,

   title={The Team},

   url={http://www21.in.tum.de/team},

   urldate={2014-06-05},

   year={2013}

 }

 @online{tum2014isainst,

   title={Installation},

   url={http://isabelle.in.tum.de/installation.html},

   urldate={2014-06-05},

   year={2013}

 }

 @online{andriusvelykis2013isaclipse,

   title={Isabelle/Eclipse},

   url={http://andriusvelykis.github.io/isabelle-eclipse/},

   urldate={2014-06-05},

   year={2013}

 }

 @online{emath2013emath,

   title={E-Math},

   url={http://emath.eu/en/},

   urldate={2014-06-05},

   year={2013}

 }

 @online{tum2013isadoc,

   title={Documentation},

   url={http://isabelle.in.tum.de/documentation.html},

   urldate={2014-06-13},

   year={2013},

   OPTnote={Theory libraries for Isabelle2013-2}

 }

 @online{wiki2014proofass,

   title={Proof assistant - Wikipedia, the free encyclopedia},

   url={http://en.wikipedia.org/wiki/Proof_assistant},

   urldate={2014-06-13},

   year={2014}

 }

 @online{wiki2014atp,

   title={Automated theorem proving - Wikipedia, the free encyclopedia},

   url={http://en.wikipedia.org/wiki/Automated_theorem_proving},

   urldate={2014-06-13},

   year={2014}

 }

 @online{tum2013isahol,

   title={Isabelle/HOL sessions},

   url={http://isabelle.in.tum.de/dist/library/HOL/},

   urldate={2014-06-13}

 }

 @online{isac2014pblequuniv,

   title={www.ist.tugraz.at/projects/isac/www/kbase/pbl/pbl\_equ\_univ.html},

   url={http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/pbl_equ_univ.html},

   urldate={2014-06-13}

 }

 @mastersthesis{haller2006object,

   title={An Object-Oriented Programming Model for Event-Based Actors},

   author={Haller, Philipp},

   year={2006},

   school={University of Karlsruhe}

 }

 @online{wenzel2014actors,

   title={Re: [isabelle-dev] scala-2.11.0},

   url={http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg05253.html},

   author={Wenzel, Makarius},

   year={2014},

   urldate={2014-06-16}

 }

 @inproceedings{blanchette2011automatic,

  author = {Blanchette, Jasmin Christian and Bulwahn, Lukas and Nipkow, Tobias},

  title = {Automatic Proof and Disproof in Isabelle/HOL},

  booktitle = {Proceedings of the 8th International Conference on Frontiers of Combining Systems},

  series = {FroCoS'11},

  year = {2011},

  isbn = {978-3-642-24363-9},

  venue = {Saarbrücken, Germany},

  pages = {12--27},

  numpages = {16},

  url = {http://dl.acm.org/citation.cfm?id=2050784.2050787},

  acmid = {2050787},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 }

 %@inproceedings{wenzel2007sml,

 %  title={SML with antiquotations embedded into Isabelle/Isar},

 %  author={Wenzel, Makarius and Chaieb, Amine},

 %  booktitle={Workshop on Programming Languages for Mechanized Mathematics (satellite of CALCULEMUS 2007). %Hagenberg, Austria},

 %  year={2007}

 %}

 @online{tum2014repo,

   title={isabelle: Summary},

   url={http://isabelle.in.tum.de/repos/isabelle/},

   year={2014},

   urldate={2014-06-21}

 }