all.bib

@article{Herlihy1990,
	author = {Herlihy, Maurice P. and Wing, Jeannette M.},
	title = {{Linearizability: A Correctness Condition for Concurrent Objects}},
	journal = {{ACM Transactions on Programming Languages and Systems}},
	issue_date = {July 1990},
	volume = {12},
	number = {3},
	month = jul,
	year = {1990},
	issn = {0164-0925},
	pages = {463--492},
	numpages = {30},
	doi = {10.1145/78969.78972},
	acmid = {78972},
	publisher = {ACM},
	address = {New York, NY, USA},
}

@inproceedings{Walter,
	author = {Sovran, Yair and Power, Russell and Aguilera, Marcos K. and Li, Jinyang},
	title = {{Transactional Storage for Geo-replicated Systems}},
	booktitle = {{Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles}},
	series = {SOSP '11},
	year = {2011},
	isbn = {978-1-4503-0977-6},
	location = {Cascais, Portugal},
	pages = {385--400},
	numpages = {16},
	doi = {10.1145/2043556.2043592},
	acmid = {2043592},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {asynchronous replication, distributed storage, geo-distributed systems, key-value store, parallel snapshot isolation, transactions},
}

@inproceedings{Berenson95,
	author = {Berenson, Hal and Bernstein, Phil and Gray, Jim and Melton, Jim and O'Neil, Elizabeth and O'Neil, Patrick},
	title = {{A Critique of ANSI SQL Isolation Levels}},
	booktitle = {{Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data}},
	series = {SIGMOD '95},
	year = {1995},
	isbn = {0-89791-731-6},
	location = {San Jose, California, USA},
	pages = {1--10},
	numpages = {10},
	doi = {10.1145/223784.223785},
	acmid = {223785},
	publisher = {ACM},
	address = {New York, NY, USA},
}

@inproceedings{Calm,
	author    = {Peter Alvaro and Neil Conway and Joe Hellerstein and William R. Marczak},
	title     = {{Consistency Analysis in Bloom: a {CALM} and Collected Approach}},
	booktitle = {{CIDR} 2011, Fifth Biennial Conference on Innovative Data Systems
		Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings},
	year      = {2011},
	pages     = {249--260},
	url       = {http://www.cidrdb.org/cidr2011/Papers/CIDR11_Paper35.pdf},
}

@inproceedings{Sieve,
	author = {Li, Cheng and Leit\~{a}o, Jo\~{a}o and Clement, Allen and Pregui\c{c}a, Nuno and Rodrigues, Rodrigo and Vafeiadis, Viktor},
	title = {{Automating the Choice of Consistency Levels in Replicated Systems}},
	booktitle = {{Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference}},
	series = {USENIX ATC'14},
	year = {2014},
	isbn = {978-1-931971-10-2},
	location = {Philadelphia, PA},
	pages = {281--292},
	numpages = {12},
	url = {http://dl.acm.org/citation.cfm?id=2643634.2643664},
	acmid = {2643664},
	publisher = {USENIX Association},
	address = {Berkeley, CA, USA},
}

@inproceedings{Eiger,
	author = {Lloyd, Wyatt and Freedman, Michael J. and Kaminsky, Michael and Andersen, David G.},
	title = {{Stronger Semantics for Low-latency Geo-replicated Storage}},
	booktitle = {{Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation}},
	series = {nsdi'13},
	year = {2013},
	location = {Lombard, IL},
	pages = {313--328},
	numpages = {16},
	url = {http://dl.acm.org/citation.cfm?id=2482626.2482657},
	acmid = {2482657},
	publisher = {USENIX Association},
	address = {Berkeley, CA, USA},
}


@inproceedings{BoltOn,
	author = {Bailis, Peter and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
	title = {{Bolt-on Causal Consistency}},
	booktitle = {{Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data}},
	series = {SIGMOD '13},
	year = {2013},
	isbn = {978-1-4503-2037-5},
	location = {New York, New York, USA},
	pages = {761--772},
	numpages = {12},
	doi = {10.1145/2463676.2465279},
	acmid = {2465279},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {causal consistency, eventual consistency, separation of concerns},
}

@incollection{SSS,
	author={Shapiro, Marc and Preguiça, Nuno and Baquero, Carlos and Zawirski, Marek},
	year={2011},
	isbn={978-3-642-24549-7},
	booktitle={{Stabilization, Safety, and Security of Distributed Systems}},
	volume={6976},
	series={Lecture Notes in Computer Science},
	editor={Défago, Xavier and Petit, Franck and Villain, Vincent},
	doi={10.1007/978-3-642-24550-3_29},
	title={{Conflict-Free Replicated Data Types}},
	publisher={Springer Berlin Heidelberg},
	keywords={Eventual Consistency; Replicated Shared Objects; Large-Scale Distributed Systems},
	pages={386-400},
	language={English}
}

@misc{Z3,
	key = {Z3},
	title={The Z3 Theorem Prover},
	url = {{https://github.com/Z3Prover/z3}},
	note = {Accessed: 2022-03-20 13:21:00},
	year = {2022}

}

@misc{mirage,
	key = {Mirage},
	title={{A programming framework for building type-safe, modular systems}},
	url = {https://mirage.io },
  note = {Accessed: 2017-01-03 12:21:00},
  year = {2013}
}

@misc{RUBiS,
	key = {RUBiS},
	title={{Rice University Bidding System}},
	url = {http://rubis.ow2.org/},
	note = {Accessed: 2014-11-4 13:21:00},
	year = {2014}

}

@misc{Twissandra,
	key = {Twissandra},
	title={{Twitter clone on Cassandra}},
	url = {http://twissandra.com/},
	note = {Accessed: 2014-11-4 13:21:00},
	year = {2014}
}

@inproceedings{YCSB,
	author = {Cooper, Brian F. and Silberstein, Adam and Tam, Erwin and Ramakrishnan, Raghu and Sears, Russell},
	title = {{Benchmarking Cloud Serving Systems with YCSB}},
	booktitle = {{Proceedings of the 1st ACM Symposium on Cloud Computing}},
	series = {SoCC '10},
	year = {2010},
	isbn = {978-1-4503-0036-0},
	location = {Indianapolis, Indiana, USA},
	pages = {143--154},
	numpages = {12},
	doi = {10.1145/1807128.1807152},
	acmid = {1807152},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {benchmarking, cloud serving database},
}


@inproceedings{Burckhardt2012,
	author = {Burckhardt, Sebastian and Leijen, Daan and F\"{a}hndrich, Manuel and Sagiv, Mooly},
	title = {{Eventually Consistent Transactions}},
	booktitle = {{Proceedings of the 21st European Conference on Programming Languages and Systems}},
	series = {ESOP'12},
	year = {2012},
	isbn = {978-3-642-28868-5},
	location = {Tallinn, Estonia},
	pages = {67--86},
	numpages = {20},
	doi = {10.1007/978-3-642-28869-2_4},
	acmid = {2259252},
	publisher = {Springer-Verlag},
	address = {Berlin, Heidelberg},
}

@article{Serializability,
	author = {Papadimitriou, Christos H.},
	title = {{The Serializability of Concurrent Database Updates}},
	journal = {{Journal of the ACM}},
	issue_date = {Oct. 1979},
	volume = {26},
	number = {4},
	month = oct,
	year = {1979},
	issn = {0004-5411},
	pages = {631--653},
	numpages = {23},
	doi = {10.1145/322154.322158},
	acmid = {322158},
	publisher = {ACM},
	address = {New York, NY, USA},
}


@misc{Brewer2000,
	author={Brewer, Eric},
	title={{Towards Robust Distributed Systems (Invited Talk)}},
	series = {PODC},
	year = {2000}
}


@article{Gilbert2002,
	author = {Gilbert, Seth and Lynch, Nancy},
	title = {{Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-tolerant Web Services}},
	journal = {SIGACT News},
	issue_date = {June 2002},
	volume = {33},
	number = {2},
	month = jun,
	year = {2002},
	issn = {0163-5700},
	pages = {51--59},
	numpages = {9},
	doi = {10.1145/564585.564601},
	acmid = {564601},
	publisher = {ACM},
	address = {New York, NY, USA},
}


@inproceedings{Dynamo,
	author = {DeCandia, Giuseppe and Hastorun, Deniz and Jampani, Madan and Kakulapati, Gunavardhan and Lakshman, Avinash and Pilchin, Alex and Sivasubramanian, Swaminathan and Vosshall, Peter and Vogels, Werner},
	title = {{Dynamo: Amazon's Highly Available Key-value Store}},
	booktitle = {{Proceedings of Twenty-first ACM SIGOPS Symposium on Operating Systems Principles}},
	series = {SOSP '07},
	year = {2007},
	isbn = {978-1-59593-591-5},
	location = {Stevenson, Washington, USA},
	pages = {205--220},
	numpages = {16},
	doi = {10.1145/1294261.1294281},
	acmid = {1294281},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {performance, reliability, scalability},
}


@article{Cassandra,
	author = {Lakshman, Avinash and Malik, Prashant},
	title = {{Cassandra: A Decentralized Structured Storage System}},
	journal = {{SIGOPS Operating Systems Review}},
	issue_date = {April 2010},
	volume = {44},
	number = {2},
	month = apr,
	year = {2010},
	issn = {0163-5980},
	pages = {35--40},
	numpages = {6},
	doi = {10.1145/1773912.1773922},
	acmid = {1773922},
	publisher = {ACM},
	address = {New York, NY, USA},
}


@inproceedings{Burckhardt2014,
	author = {Burckhardt, Sebastian and Gotsman, Alexey and Yang, Hongseok and Zawirski, Marek},
	title = {{Replicated Data Types: Specification, Verification, Optimality}},
	booktitle = {{Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}},
	series = {POPL '14},
	year = {2014},
	isbn = {978-1-4503-2544-8},
	location = {San Diego, California, USA},
	pages = {271--284},
	numpages = {14},
	doi = {10.1145/2535838.2535848},
	acmid = {2535848},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {eventual consistency, replication, weak memory},
}

@inproceedings{Pileus,
	author = {Terry, Douglas B. and Prabhakaran, Vijayan and Kotla, Ramakrishna and Balakrishnan, Mahesh and Aguilera, Marcos K. and Abu-Libdeh, Hussam},
	title = {{Consistency-based Service Level Agreements for Cloud Storage}},
	booktitle = {{Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles}},
	series = {SOSP '13},
	year = {2013},
	isbn = {978-1-4503-2388-8},
	location = {Farminton, Pennsylvania},
	pages = {309--324},
	numpages = {16},
	doi = {10.1145/2517349.2522731},
	acmid = {2522731},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {cloud computing, consistency, replication, service level agreement, storage},
}

@inproceedings{RedBlue,
	author = {Li, Cheng and Porto, Daniel and Clement, Allen and Gehrke, Johannes and Pregui\c{c}a, Nuno and Rodrigues, Rodrigo},
	title = {{Making Geo-replicated Systems Fast As Possible, Consistent when Necessary}},
	booktitle = {{Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation}},
	series = {OSDI'12},
	year = {2012},
	isbn = {978-1-931971-96-6},
	location = {Hollywood, CA, USA},
	pages = {265--278},
	numpages = {14},
	url = {http://dl.acm.org/citation.cfm?id=2387880.2387906},
	acmid = {2387906},
	publisher = {USENIX Association},
	address = {Berkeley, CA, USA},
}


@article{IConfluence,
	author    = {Peter Bailis and Alan Fekete and Michael J. Franklin and Ali Ghodsi and Joseph M. Hellerstein and Ion Stoica},
	title     = {{Coordination-Avoiding Database Systems}},
	journal   = {CoRR},
	year      = {2014},
	volume    = {abs/1402.2237},
	url       = {http://arxiv.org/abs/1402.2237},
}

@article{BailisHAT,
	author = {Peter Bailis and Aaron Davidson and Alan Fekete and Ali Ghodsi and Joseph M. Hellerstein and Ion Stoica},
	title     = {{Highly Available Transactions: Virtues and Limitations}},
	journal   = {PVLDB},
	volume    = {7},
	number    = {3},
	year      = {2013},
	pages     = {181-192},
	ee        = {http://www.vldb.org/pvldb/vol7/p181-bailis.pdf},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{COPS,
	author = {Lloyd, Wyatt and Freedman, Michael J. and Kaminsky, Michael and Andersen, David G.},
	title = {{Don't Settle for Eventual: Scalable Causal Consistency for Wide-area Storage with COPS}},
	booktitle = {{Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles}},
	series = {SOSP '11},
	year = {2011},
	isbn = {978-1-4503-0977-6},
	location = {Cascais, Portugal},
	pages = {401--416},
	numpages = {16},
	doi = {10.1145/2043556.2043593},
	acmid = {2043593},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {ALPS systems, causal + consistency, key-value storage, read transactions, scalable wide-area replication},
}

@inproceedings{Session,
	author = {Terry, Douglas B. and Demers, Alan J. and Petersen, Karin and Spreitzer, Mike and Theimer, Marvin and Welch, Brent W.},
	title = {{Session Guarantees for Weakly Consistent Replicated Data}},
	booktitle = {{Proceedings of the Third International Conference on Parallel and Distributed Information Systems}},
	series = {PDIS '94},
	year = {1994},
	isbn = {0-8186-6400-2},
	pages = {140--149},
	numpages = {10},
	url = {http://dl.acm.org/citation.cfm?id=645792.668302},
	acmid = {668302},
	publisher = {IEEE Computer Society},
	address = {Washington, DC, USA},
}

@inproceedings{Tango,
	author = {Balakrishnan, Mahesh and Malkhi, Dahlia and Wobber, Ted and Wu, Ming and Prabhakaran, Vijayan and Wei, Michael and Davis, John D. and Rao, Sriram and Zou, Tao and Zuck, Aviad},
	title = {{Tango: Distributed Data Structures over a Shared Log}},
	booktitle = {{Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles}},
	series = {SOSP '13},
	year = {2013},
	isbn = {978-1-4503-2388-8},
	location = {Farminton, Pennsylvania},
	pages = {325--340},
	numpages = {16},
	doi = {10.1145/2517349.2522732},
	acmid = {2522732},
	publisher = {ACM},
	address = {New York, NY, USA},
}

@inproceedings{indigo,
  author = {Valter Balegas and Nuno Pregui{\c c}a and Rodrigo Rodrigues and S{\'e}rgio Duarte and Carla Ferreira and Mahsa Najafzadeh and Marc Shapiro},
  title =  {{Putting the Consistency back into Eventual Consistency}},
  booktitle = {{Proceedings of the Tenth European Conference on Computer System}},
  year = {2015},
  series = {EuroSys '15},
  address =  {Bordeaux, France},
  url =   {http://lip6.fr/Marc.Shapiro/papers/putting-consistency-back-EuroSys-2015.pdf}
}

@inproceedings{Burckhardt2015,
 author = {Sebastian Burckhardt and Daan Leijen and Jonathan Protzenko and Manuel F\"{a}hndrich},
 title = {{Global Sequence Protocol: A Robust Abstraction for Replicated Shared State}},
 booktitle = {{Proceedings of the 29th European Conference on Object-Oriented Programming}},
year = {2015},
 series = {ECOOP '15},
 address = {Prague, Czech Republic},
 url = {http://research.microsoft.com/pubs/240462/gsp-tr-2015-2.pdf}
}

@techreport{techrep,
  author = {{KC Sivaramakrishnan} and Gowtham Kaki and Suresh Jagannathan},
  title = {{Declarative Programming over Eventually Consistent Data
          Store}},
  institution = {Purdue University},
  number = {TR-15-002},
  url = {http://docs.lib.purdue.edu/cstech/1776/},
  year = 2015}


@inproceedings{WWP+15,
 author = {Wilcox, James R. and Woos, Doug and Panchekha, Pavel and Tatlock, Zachary and Wang, Xi and Ernst, Michael D. and Anderson, Thomas},
 title = {{Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}},
 booktitle = {PLDI},
 year = {2015},
 pages = {357--368},
}


@inproceedings{CDE+12,
 author = {Corbett, James C. and Dean, Jeffrey and Epstein, Michael and Fikes, Andrew and Frost, Christopher and Furman, J. J. and Ghemawat, Sanjay and Gubarev, Andrey and Heiser, Christopher and Hochschild, Peter and Hsieh, Wilson and Kanthak, Sebastian and Kogan, Eugene and Li, Hongyi and Lloyd, Alexander and Melnik, Sergey and Mwaura, David and Nagle, David and Quinlan, Sean and Rao, Rajesh and Rolig, Lindsay and Saito, Yasushi and Szymaniak, Michal and Taylor, Christopher and Wang, Ruth and Woodford, Dale},
 title = {{Spanner: Google's Globally-distributed Database}},
 booktitle = {Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation},
 series = {OSDI'12},
 year = {2012},
 isbn = {978-1-931971-96-6},
 location = {Hollywood, CA, USA},
 pages = {251--264},
 numpages = {14},
 url = {http://dl.acm.org/citation.cfm?id=2387880.2387905},
 acmid = {2387905},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
}

@inproceedings{DNN+15,
 author = {Dragojevi\'{c}, Aleksandar and Narayanan, Dushyanth and Nightingale, Edmund B. and Renzelmann, Matthew and Shamis, Alex and Badam, Anirudh and Castro, Miguel},
 title = {No Compromises: Distributed Transactions with Consistency, Availability, and Performance},
 booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles},
 series = {SOSP '15},
 year = {2015},
 isbn = {978-1-4503-3834-9},
 location = {Monterey, California},
 pages = {54--70},
 numpages = {17},
 url = {http://doi.acm.org/10.1145/2815400.2815425},
 doi = {10.1145/2815400.2815425},
 acmid = {2815425},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{BFL+12,
 author = {Burckhardt, Sebastian and F\"{a}hndrich, Manuel and Leijen, Daan and Wood, Benjamin P.},
 title = {{Cloud Types for Eventual Consistency}},
 booktitle = {Proceedings of the 26th European Conference on Object-Oriented Programming},
 series = {ECOOP'12},
 year = {2012},
 isbn = {978-3-642-31056-0},
 location = {Beijing, China},
 pages = {283--307},
 numpages = {25},
 url = {http://dx.doi.org/10.1007/978-3-642-31057-7_14},
 doi = {10.1007/978-3-642-31057-7_14},
 acmid = {2367183},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@inproceedings{crdts,
 author = {Shapiro, Marc and Pregui\c{c}a, Nuno and Baquero, Carlos and Zawirski, Marek},
 title = {Conflict-free Replicated Data Types},
 booktitle = {Proceedings of the 13th International Conference on Stabilization, Safety, and Security of Distributed Systems},
 series = {SSS'11},
 year = {2011},
 isbn = {978-3-642-24549-7},
 location = {Grenoble, France},
 pages = {386--400},
 numpages = {15},
 url = {http://dl.acm.org/citation.cfm?id=2050613.2050642},
 acmid = {2050642},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 keywords = {eventual consistency, large-scale distributed systems, replicated shared objects},
}

@book{Armstrong07,
 author = {Armstrong, Joe},
 title = {Programming Erlang: Software for a Concurrent World},
 year = {2007},
 isbn = {193435600X, 9781934356005},
 publisher = {Pragmatic Bookshelf},
}

@misc(Irmin,
 key = {Irmin},
  note = {Irmin: https://mirage.io/blog/introducing-irmin},
  year = 2016)


@inproceedings{BBL+10,
 key = {Burckhardt},
 author = {Burckhardt, Sebastian and Baldassin, Alexandro and Leijen, Daan},
 title = {Concurrent Programming with Revisions and Isolation Types},
 booktitle = {Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications},
 series = {OOPSLA '10},
 year = {2010},
 isbn = {978-1-4503-0203-6},
 location = {Reno/Tahoe, Nevada, USA},
 pages = {691--707},
 numpages = {17},
 url = {http://doi.acm.org/10.1145/1869459.1869515},
 doi = {10.1145/1869459.1869515},
 acmid = {1869515},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrency, isolation, parallelism, revisions, transactions},
}


@inproceedings{BEG+17,
 key = {Bouajjani},
 author = {Bouajjani, Ahmed and Enea, Constantin and Guerraoui, Rachid and Hamza, Jad},
 title = {On Verifying Causal Consistency},
 booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 series = {POPL 2017},
 year = {2017},
 isbn = {978-1-4503-4660-3},
 location = {Paris, France},
 pages = {626--638},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/3009837.3009888},
 doi = {10.1145/3009837.3009888},
 acmid = {3009888},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {causal consistency, distributed systems, model checking, static program analysis},
}


@inproceedings{exokernel,
 author = {Engler, D. R. and Kaashoek, M. F. and O'Toole,Jr., J.},
 title = {Exokernel: An Operating System Architecture for Application-level Resource Management},
 booktitle = {Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles},
 series = {SOSP '95},
 year = {1995},
 isbn = {0-89791-715-4},
 location = {Copper Mountain, Colorado, USA},
 pages = {251--266},
 numpages = {16},
 url = {http://doi.acm.org/10.1145/224056.224076},
 doi = {10.1145/224056.224076},
 acmid = {224076},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@article{nemesis,
 author = {Leslie, I. M. and McAuley, D. and Black, R. and Roscoe, T. and Barham, P. and Evers, D. and Fairbairns, R. and Hyden, E.},
 title = {The Design and Implementation of an Operating System to Support Distributed Multimedia Applications},
 journal = {IEEE J.Sel. A. Commun.},
 issue_date = {September 2006},
 volume = {14},
 number = {7},
 month = sep,
 year = {2006},
 issn = {0733-8716},
 pages = {1280--1297},
 numpages = {18},
 url = {http://dx.doi.org/10.1109/49.536480},
 doi = {10.1109/49.536480},
 acmid = {2312461},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
}
@article{unikernels,
 author = {Madhavapeddy, Anil and Scott, David J.},
 title = {Unikernels: Rise of the Virtual Library Operating System},
 journal = {Queue},
 issue_date = {November 2013},
 volume = {11},
 number = {11},
 month = dec,
 year = {2013},
 issn = {1542-7730},
 pages = {30:30--30:44},
 articleno = {30},
 numpages = {15},
 url = {http://doi.acm.org/10.1145/2557963.2566628},
 doi = {10.1145/2557963.2566628},
 acmid = {2566628},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@misc{dhh-quote,
  key={D. H. Hansson},
  title={Choose a single layer of cleverness},
  url={http://david.heinemeierhansson.com/arc/2005_09.html},
  note = {Accessed: 2017-01-03 12:21:00},
  year = {2005}
}
@inproceedings{bailis-sigmod15,
 author = {Bailis, Peter and Fekete, Alan and Franklin, Michael J. and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
 title = {Feral Concurrency Control: An Empirical Investigation of Modern Application Integrity},
 booktitle = {Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data},
 series = {SIGMOD '15},
 year = {2015},
 isbn = {978-1-4503-2758-9},
 location = {Melbourne, Victoria, Australia},
 pages = {1327--1342},
 numpages = {16},
 url = {http://doi.acm.org/10.1145/2723372.2737784},
 doi = {10.1145/2723372.2737784},
 acmid = {2737784},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {application integrity, concurrency control, impedance mismatch, invariants, orms, ruby on rails},
}

@inproceedings{ireland09,
 author = {Ireland, Christopher and Bowers, David and Newton, Michael and Waugh, Kevin},
 title = {A Classification of Object-Relational Impedance Mismatch},
 booktitle = {Proceedings of the 2009 First International Conference on Advances in Databases, Knowledge, and Data Applications},
 series = {DBKDA '09},
 year = {2009},
 isbn = {978-0-7695-3550-0},
 pages = {36--43},
 numpages = {8},
 url = {http://dx.doi.org/10.1109/DBKDA.2009.11},
 doi = {10.1109/DBKDA.2009.11},
 acmid = {1545492},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {Object-Relational, Classification, Impedance Mismatch, ORM, Database, SQL},
}
@misc{activerecord,
  key={Rails Guides},
  title={Active Record Basics},
  url={http://guides.rubyonrails.org/active_record_basics.html},
  note = {Accessed: 2017-01-03 13:00:00},
  year = {2017}
}
@book{hibernate,
 author = {Bauer, Christian and King, Gavin},
 title = {Java Persistence with Hibernate},
 year = {2006},
 isbn = {1932394885},
 publisher = {Manning Publications Co.},
 address = {Greenwich, CT, USA},
}
@article{zoo,
  author    = {Paolo Viotti and
               Marko Vukolic},
  title     = {{Consistency in Non-Transactional Distributed Storage Systems}},
  journal   = {CoRR},
  volume    = {abs/1512.00168},
  year      = {2015},
  url       = {http://arxiv.org/abs/1512.00168},
  timestamp = {Sat, 02 Jan 2016 11:38:49 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/ViottiV15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{berenson95,
	author = {Berenson, Hal and Bernstein, Phil and Gray, Jim and Melton, Jim and O'Neil, Elizabeth and O'Neil, Patrick},
	title = {{A Critique of ANSI SQL Isolation Levels}},
	booktitle = {{Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data}},
	series = {SIGMOD '95},
	year = {1995},
	isbn = {0-89791-731-6},
	location = {San Jose, California, USA},
	pages = {1--10},
	numpages = {10},
	doi = {10.1145/223784.223785},
	acmid = {223785},
	publisher = {ACM},
	address = {New York, NY, USA},
}
@inproceedings{bailis-bolton,
	author = {Bailis, Peter and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
	title = {{Bolt-on Causal Consistency}},
	booktitle = {{Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data}},
	series = {SIGMOD '13},
	year = {2013},
	isbn = {978-1-4503-2037-5},
	location = {New York, New York, USA},
	pages = {761--772},
	numpages = {12},
	doi = {10.1145/2463676.2465279},
	acmid = {2465279},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {causal consistency, eventual consistency, separation of concerns},
}
@inproceedings{fgm15,
  title={{Mergeable persistent data structures}},
  author={Farinier, Benjamin and Gazagnaire, Thomas and Madhavapeddy, Anil},
  booktitle={Vingt-sixi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2015)},
  year={2015}
}
@inproceedings{jitsu,
 author = {Madhavapeddy, Anil and Leonard, Thomas and Skjegstad, Magnus and Gazagnaire, Thomas and Sheets, David and Scott, Dave and Mortier, Richard and Chaudhry, Amir and Singh, Balraj and Ludlam, Jon and Crowcroft, Jon and Leslie, Ian},
 title = {Jitsu: Just-in-time Summoning of Unikernels},
 booktitle = {Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation},
 series = {NSDI'15},
 year = {2015},
 isbn = {978-1-931971-218},
 location = {Oakland, CA},
 pages = {559--573},
 numpages = {15},
 url = {http://dl.acm.org/citation.cfm?id=2789770.2789809},
 acmid = {2789809},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
}
@misc{eu-model-clauses,
  key={Microsoft Trust Center},
  title={European Union Model Clauses},
  url={https://www.microsoft.com/en-us/TrustCenter/Compliance/EU-Model-Clauses},
  note = {Accessed: 2017-01-03 13:00:00},
  year = {2017}
}
@inproceedings{malpani10,
  title   = {Reverse engineering models from databases to bootstrap
      application development},
  author  = {Malpani, Ankit and others},
  booktitle = {ICDE},
  year    = {2010}
}
@article{bailis-vldb,
 author = {Bailis, Peter and Fekete, Alan and Franklin, Michael J. and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
 title = {{Coordination Avoidance in Database Systems}},
 journal = {Proc. VLDB Endow.},
 issue_date = {November 2014},
 volume = {8},
 number = {3},
 month = nov,
 year = {2014},
 issn = {2150-8097},
 pages = {185--196},
 numpages = {12},
 url = {http://dx.doi.org/10.14778/2735508.2735509},
 doi = {10.14778/2735508.2735509},
 acmid = {2735509},
 publisher = {VLDB Endowment},
}
@inproceedings{alvaro-calm,
	author    = {Peter Alvaro and Neil Conway and Joe Hellerstein and William R. Marczak},
	title     = {{Consistency Analysis in Bloom: a {CALM} and Collected Approach}},
	booktitle = {{CIDR} 2011, Fifth Biennial Conference on Innovative Data Systems
		Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings},
	year      = {2011},
	pages     = {249--260},
}
@inproceedings{gotsman-popl16,
 author = {Gotsman, Alexey and Yang, Hongseok and Ferreira, Carla and Najafzadeh, Mahsa and Shapiro, Marc},
 title = {{'Cause I'm Strong Enough: Reasoning About Consistency Choices in Distributed Systems}},
 booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL 2016},
 year = {2016},
 isbn = {978-1-4503-3549-2},
 location = {St. Petersburg, FL, USA},
 pages = {371--384},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2837614.2837625},
 doi = {10.1145/2837614.2837625},
 acmid = {2837625},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Replication, causal consistency, integrity invariants},
}
@inproceedings{redblue-osdi,
	author = {Li, Cheng and Porto, Daniel and Clement, Allen and Gehrke, Johannes and Pregui\c{c}a, Nuno and Rodrigues, Rodrigo},
	title = {{{Making Geo-replicated Systems Fast As Possible, Consistent when Necessary}}},
	booktitle = {{Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation}},
	series = {OSDI'12},
	year = {2012},
	isbn = {978-1-931971-96-6},
	location = {Hollywood, CA, USA},
	pages = {265--278},
	numpages = {14},
	url = {http://dl.acm.org/citation.cfm?id=2387880.2387906},
	acmid = {2387906},
	publisher = {USENIX Association},
	address = {Berkeley, CA, USA},
}
@inproceedings{redblue-atc,
	author = {Li, Cheng and Leit\~{a}o, Jo\~{a}o and Clement, Allen and Pregui\c{c}a, Nuno and Rodrigues, Rodrigo and Vafeiadis, Viktor},
	title = {{Automating the Choice of Consistency Levels in Replicated Systems}},
	booktitle = {{Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference}},
	series = {USENIX ATC'14},
	year = {2014},
	isbn = {978-1-931971-10-2},
	location = {Philadelphia, PA},
	pages = {281--292},
	numpages = {12},
	url = {http://dl.acm.org/citation.cfm?id=2643634.2643664},
	acmid = {2643664},
	publisher = {USENIX Association},
	address = {Berkeley, CA, USA},
}
@inproceedings{ecinec,
  author = {Valter Balegas and Nuno Pregui{\c c}a and Rodrigo Rodrigues and S{\'e}rgio Duarte and Carla Ferreira and Mahsa Najafzadeh and Marc Shapiro},
  title =  {{{Putting the Consistency back into Eventual Consistency}}},
  booktitle = {{Proceedings of the Tenth European Conference on Computer System}},
  year = {2015},
  series = {EuroSys '15},
  address =  {Bordeaux, France},
  url =   {http://lip6.fr/Marc.Shapiro/papers/putting-consistency-back-EuroSys-2015.pdf}
}
@inproceedings{lbc16,
 author = {Lesani, Mohsen and Bell, Christian J. and Chlipala, Adam},
 title = {{Chapar: Certified Causally Consistent Distributed Key-value Stores}},
 booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '16},
 year = {2016},
 isbn = {978-1-4503-3549-2},
 location = {St. Petersburg, FL, USA},
 pages = {357--370},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2837614.2837622},
 doi = {10.1145/2837614.2837622},
 acmid = {2837622},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {causal consistency, theorem proving, verification},
}

@inproceedings{verdi,
 author = {Wilcox, James R. and Woos, Doug and Panchekha, Pavel and Tatlock, Zachary and Wang, Xi and Ernst, Michael D. and Anderson, Thomas},
 title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems},
 booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '15},
 year = {2015},
 isbn = {978-1-4503-3468-6},
 location = {Portland, OR, USA},
 pages = {357--368},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2737924.2737958},
 doi = {10.1145/2737924.2737958},
 acmid = {2737958},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Coq, Formal verification, Verdi, distributed systems, proof assistants},
}

@inproceedings{vietnam,
 author = {Ted Neward},
 title = {The Vietnam of Computer Science},
 year = {2006},
 booktitle = {ODBMS.ORG, News},
 url = {http://www.odbms.org/About/News/20070521.aspx},
}
@misc{ormhate,
  key={Martin Fowler},
  title={OrmHate},
  url={http://martinfowler.com/bliki/OrmHate.html},
  note = {Accessed: 2017-01-04 12:00:00},
  year = {2012}
}
@inproceedings{carey-turmoil96,
  title   = {Of objects and databases: A decade of turmoil},
  author  = {Carey, Michael J and DeWitt, David J},
  booktitle = {VLDB},
  year    = {1996}
}

@inproceedings{macros,
	author = {Yallop, Jeremy and White, Leo},
	title = {{Modular Macros}},
	booktitle = {{Proceedings of the 2015 OCaml Users and Developers Workshop}},
	series = {OCaml'15},
	year = {2015},
	url={https://www.cl.cam.ac.uk/~jdy22/papers/modular-macros.pdf},
	location = {Vancouver, Canada},
}
@misc{ec2instances,
	key={Amazon Ec2 Instances},
	title={{Amazon Ec2 Instances}},
	url={https://aws.amazon.com/ec2/instance-types/},
	note = {Accessed: 2017-01-04 10:12:00},
	year = {2017},
}
@misc{functoria,
	key={Functoria},
	title={{Functoria: A DSL to invoke otherworldly functors}},
	url={https://github.com/mirage/functoria},
	note = {Accessed: 2017-01-04 10:12:00},
	year = {2017},
}
@misc{git,
	key={Git},
	title={{Git: a free and open source distributed version control system}},
	utl={https://git-scm.com/},
	note = {Accessed: 2017-01-04 10:12:00},
	year = {2017},
}
@misc{git-tp,
	key={Git Transfer Protocol},
	title={{Git Internals -- Transfer Protocols}},
	utl={https://git-scm.com/book/en/v2/Git-Internals-Transfer-Protocols},
	note = {Accessed: 2017-01-04 10:12:00},
	year = {2017},
}
@misc{gcp,
	key={GCP},
	title={{Google Cloud Platform}},
	utl={https://cloud.google.com/},
	note = {Accessed: 2017-01-04 10:12:00},
	year = {2017},
}
@misc{ppx,
	key={PPX},
	title={{PPX extension points}},
	utl={https://ocaml.io/w/PPX},
	note = {Accessed: 2017-01-04 10:12:00},
	year = {2017},
}
@inproceedings{terry-pdis94,
	author = {Terry, Douglas B. and Demers, Alan J. and Petersen, Karin and Spreitzer, Mike and Theimer, Marvin and Welch, Brent W.},
	title = {{Session Guarantees for Weakly Consistent Replicated Data}},
	booktitle = {{Proceedings of the Third International Conference on Parallel and Distributed Information Systems}},
	series = {PDIS '94},
	year = {1994},
	isbn = {0-8186-6400-2},
	pages = {140--149},
	numpages = {10},
	url = {http://dl.acm.org/citation.cfm?id=645792.668302},
	acmid = {668302},
	publisher = {IEEE Computer Society},
	address = {Washington, DC, USA},
}
@inproceedings{burckhardt-popl14,
	author = {Burckhardt, Sebastian and Gotsman, Alexey and Yang, Hongseok and Zawirski, Marek},
	title = {{Replicated Data Types: Specification, Verification, Optimality}},
	booktitle = {{Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}},
	series = {POPL '14},
	year = {2014},
	isbn = {978-1-4503-2544-8},
	location = {San Diego, California, USA},
	pages = {271--284},
	numpages = {14},
	doi = {10.1145/2535838.2535848},
	acmid = {2535848},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {eventual consistency, replication, weak memory},
}


@Inbook{Mat97,
author="Matthews, David",
editor="Nielson, Flemming",
title= {{Concurrency in Poly/ML}},
bookTitle="ML with Concurrency: Design, Analysis, Implementation, and Application",
year="1997",
publisher="Springer New York",
address="New York, NY",
pages="31--58",
isbn="978-1-4612-2274-3",
doi="10.1007/978-1-4612-2274-3_3",
url="http://dx.doi.org/10.1007/978-1-4612-2274-3_3"
}

@article{CJK95,
 author = {Cejtin, Henry and Jagannathan, Suresh and Kelsey, Richard},
 title = {{Higher-order Distributed Objects}},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {Sept. 1995},
 volume = {17},
 number = {5},
 month = sep,
 year = {1995},
 issn = {0164-0925},
 pages = {704--739},
 numpages = {36},
 url = {http://doi.acm.org/10.1145/213978.213986},
 doi = {10.1145/213978.213986},
 acmid = {213986},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrency, continuations, higher-order languages, message-passing},
}

@Inbook{TLK+93,
author="Thomsen, Bent
and Leth, Lone
and Giacalone, Alessandro",
editor="de Bakker, J. W.
and de Roever, W. -P.
and Rozenberg, G.",
title= {{Some Issues in the Semantics of Facile Distributed Programming}},
bookTitle="Semantics: Foundations and Applications: REX Workshop Beekbergen, The Netherlands, June 1--4, 1992 Proceedings",
year="1993",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="563--593",
isbn="978-3-540-47595-8",
doi="10.1007/3-540-56596-5_47",
url="http://dx.doi.org/10.1007/3-540-56596-5_47"
}


@inproceedings{EBPJ11,
 author = {Epstein, Jeff and Black, Andrew P. and Peyton-Jones, Simon},
 title = {{Towards Haskell in the Cloud}},
 booktitle = {Proceedings of the 4th ACM Symposium on Haskell},
 series = {Haskell '11},
 year = {2011},
 isbn = {978-1-4503-0860-1},
 location = {Tokyo, Japan},
 pages = {118--129},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2034675.2034690},
 doi = {10.1145/2034675.2034690},
 acmid = {2034690},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {erlang, haskell, message-passing},
}

@inproceedings{Car95,
 author = {Cardelli, Luca},
 title = {{A Language with Distributed Scope}},
 booktitle = {Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '95},
 year = {1995},
 isbn = {0-89791-692-1},
 location = {San Francisco, California, USA},
 pages = {286--297},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/199448.199516},
 doi = {10.1145/199448.199516},
 acmid = {199516},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{BSS+06,
 author = {Billings, John and Sewell, Peter and Shinwell, Mark and Strni\v{s}a, Rok},
 title = {{Type-safe Distributed Programming for OCaml}},
 booktitle = {Proceedings of the 2006 Workshop on ML},
 series = {ML '06},
 year = {2006},
 isbn = {1-59593-483-9},
 location = {Portland, Oregon, USA},
 pages = {20--31},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1159876.1159881},
 doi = {10.1145/1159876.1159881},
 acmid = {1159881},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {HashCaml, objective Caml, type-safe marshalling},
}

@inproceedings{SLW+05,
 author = {Sewell, Peter and Leifer, James J. and Wansbrough, Keith and Nardelli, Francesco Zappa and Allen-Williams, Mair and Habouzit, Pierre and Vafeiadis, Viktor},
 title = {{Acute: High-level Programming Language Design for Distributed Computation}},
 booktitle = {Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '05},
 year = {2005},
 isbn = {1-59593-064-7},
 location = {Tallinn, Estonia},
 pages = {15--26},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1086365.1086370},
 doi = {10.1145/1086365.1086370},
 acmid = {1086370},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {ML, abstract types, distributed programming, marshalling, modules, programming languages, rebinding, serialisation, type theory, version control},
}
@book(Armstrong,
  title = {{Programmoing Erlang: Software for a Concurrent World}},
  author = {Joe Armstrong},
  publisher = {Pragmatic Bookshelf},
  year = 2007)

@inproceedings{wadler-monad,
	author = {Wadler, Philip},
	title = {Monads for Functional Programming},
	booktitle = {Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text},
	year = {1995},
	isbn = {3-540-59451-5},
	pages = {24--52},
	numpages = {29},
	url = {http://dl.acm.org/citation.cfm?id=647698.734146},
	acmid = {734146},
	publisher = {Springer-Verlag},
	address = {London, UK, UK},
}

@article{wagner-fischer,
	author = {Wagner, Robert A. and Fischer, Michael J.},
	title = {The String-to-String Correction Problem},
	journal = {J. ACM},
	issue_date = {Jan. 1974},
	volume = {21},
	number = {1},
	month = jan,
	year = {1974},
	issn = {0004-5411},
	pages = {168--173},
	numpages = {6},
	url = {http://doi.acm.org/10.1145/321796.321811},
	doi = {10.1145/321796.321811},
	acmid = {321811},
	publisher = {ACM},
	address = {New York, NY, USA},
}

@inproceedings(implicits,
  key = {White},
  title = {{Modular Implicits}},
  booktitle = {{ML Workshop}},
  year = 2014)

@inproceedings{Orleans,
	author = {Bykov, Sergey and Geller, Alan and Kliot, Gabriel and Larus, James R. and Pandya, Ravi and Thelin, Jorgen},
	title = {{Orleans: Cloud Computing for Everyone}},
	booktitle = {Proceedings of the 2Nd ACM Symposium on Cloud Computing},
	series = {SOCC '11},
	year = {2011},
	isbn = {978-1-4503-0976-9},
	location = {Cascais, Portugal},
	pages = {16:1--16:14},
	articleno = {16},
	numpages = {14},
	url = {http://doi.acm.org/10.1145/2038916.2038932},
	doi = {10.1145/2038916.2038932},
	acmid = {2038932},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {cloud computing, distributed actors, programming models},
}


@inproceedings{Padon:2016ew,
 author = {Padon, Oded and McMillan, Kenneth L. and Panda, Aurojit and Sagiv, Mooly and Shoham, Sharon},
 title = {{Ivy: Safety Verification by Interactive Generalization}},
 booktitle = {Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '16},
 year = {2016},
 isbn = {978-1-4503-4261-2},
 location = {Santa Barbara, CA, USA},
 pages = {614--630},
 numpages = {17},
 url = {http://doi.acm.org/10.1145/2908080.2908118},
 doi = {10.1145/2908080.2908118},
 acmid = {2908118},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {counterexamples to induction, distributed systems, invariant inference, safety verification},
} 

@article{PL+17,
 author = {Padon, Oded and Losa, Giuliano and Sagiv, Mooly and Shoham, Sharon},
 title = {Paxos Made EPR: Decidable Reasoning About Distributed Protocols},
 journal = {Proc. ACM Program. Lang.},
 issue_date = {October 2017},
 volume = {1},
 number = {OOPSLA},
 month = oct,
 year = {2017},
 issn = {2475-1421},
 pages = {108:1--108:31},
 articleno = {108},
 numpages = {31},
 url = {http://doi.acm.org/10.1145/3140568},
 doi = {10.1145/3140568},
 acmid = {3140568},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Paxos, deductive verification, distributed systems, effectively propositional logic, inductive invariants, safety verification},
} 
[download]

@article{PH+18,
 author = {Padon, Oded and Hoenicke, Jochen and Losa, Giuliano and Podelski, Andreas and Sagiv, Mooly and Shoham, Sharon},
 title = {{Reducing Liveness to Safety in First-order Logic}},
 journal = {Proc. ACM Program. Lang.},
 issue_date = {January 2018},
 volume = {2},
 number = {POPL},
 month = dec,
 year = {2017},
 issn = {2475-1421},
 pages = {26:1--26:33},
 articleno = {26},
 numpages = {33},
 url = {http://doi.acm.org/10.1145/3158114},
 doi = {10.1145/3158114},
 acmid = {3158114},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Liveness-to-safety reduction, first-order temporal logic},
} 

@article{twopl,
 author = {Eswaran, K. P. and Gray, J. N. and Lorie, R. A. and Traiger, I. L.},
 title = {{The Notions of Consistency and Predicate Locks in a Database System}},
 journal = {Commun. ACM},
 issue_date = {Nov. 1976},
 volume = {19},
 number = {11},
 month = nov,
 year = {1976},
 issn = {0001-0782},
 pages = {624--633},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/360363.360369},
 doi = {10.1145/360363.360369},
 acmid = {360369},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrancy, consistency, database, lock, transaction},
}
@book{ullmanbook,
 author = {Garcia-Molina, Hector and Ullman, Jeffrey D. and Widom, Jennifer},
 title = {{Database Systems: The Complete Book}},
 year = {2008},
 isbn = {9780131873254},
 edition = {2},
 publisher = {Prentice Hall Press},
 address = {Upper Saddle River, NJ, USA},
}
@book{dbtuningbook,
 author = {Shasha, Dennis and Bonnet, Philippe},
 title = {{Database Tuning: Principles, Experiments, and Troubleshooting Techniques}},
 year = {2003},
 isbn = {1-55860-753-6},
 publisher = {Morgan Kaufmann Publishers Inc.},
 address = {San Francisco, CA, USA},
} 
@inproceedings{gray1976,
    author = {J. N. Gray and R. A. Lorie and G. R. Putzolu and I. L. Traiger},
    title = {{Granularity of Locks and Degrees of Consistency in a Shared Data Base}},
    booktitle = {},
    year = {1976},
    pages = {365--394}
}
@article{cap,
	author = {Gilbert, Seth and Lynch, Nancy},
	title = {{{Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-tolerant Web Services}}},
	journal = {SIGACT News},
	issue_date = {June 2002},
	volume = {33},
	number = {2},
	month = jun,
	year = {2002},
	issn = {0163-5700},
	pages = {51--59},
	numpages = {9},
	doi = {10.1145/564585.564601},
	acmid = {564601},
	publisher = {ACM},
	address = {New York, NY, USA},
}
@inproceedings{redblueosdi,
	author = {Li, Cheng and Porto, Daniel and Clement, Allen and Gehrke, Johannes and Pregui\c{c}a, Nuno and Rodrigues, Rodrigo},
	title = {{{Making Geo-replicated Systems Fast As Possible, Consistent when Necessary}}},
	booktitle = {{Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation}},
	series = {OSDI'12},
	year = {2012},
	isbn = {978-1-931971-96-6},
	location = {Hollywood, CA, USA},
	pages = {265--278},
	numpages = {14},
	url = {http://dl.acm.org/citation.cfm?id=2387880.2387906},
	acmid = {2387906},
	publisher = {USENIX Association},
	address = {Berkeley, CA, USA},
}
@inproceedings{redblueatc,
	author = {Li, Cheng and Leit\~{a}o, Jo\~{a}o and Clement, Allen and Pregui\c{c}a, Nuno and Rodrigues, Rodrigo and Vafeiadis, Viktor},
	title = {{Automating the Choice of Consistency Levels in Replicated Systems}},
	booktitle = {{Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference}},
	series = {USENIX ATC'14},
	year = {2014},
	isbn = {978-1-931971-10-2},
	location = {Philadelphia, PA},
	pages = {281--292},
	numpages = {12},
	url = {http://dl.acm.org/citation.cfm?id=2643634.2643664},
	acmid = {2643664},
	publisher = {USENIX Association},
	address = {Berkeley, CA, USA},
}

@inproceedings{alvarocalm,
	author    = {Peter Alvaro and Neil Conway and Joe Hellerstein and William R. Marczak},
	title     = {{Consistency Analysis in Bloom: a {CALM} and Collected Approach}},
	booktitle = {{CIDR} 2011, Fifth Biennial Conference on Innovative Data Systems
		Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings},
	year      = {2011},
	pages     = {249--260},
}
@inproceedings{bailishotos,
 author = {Bailis, Peter and Fekete, Alan and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
 title = {{HAT, Not CAP: Towards Highly Available Transactions}},
 booktitle = {Proceedings of the 14th USENIX Conference on Hot Topics in Operating Systems},
 series = {HotOS'13},
 year = {2013},
 location = {Santa Ana Pueblo, New Mexcio},
 pages = {24--24},
 numpages = {1},
 url = {http://dl.acm.org/citation.cfm?id=2490483.2490507},
 acmid = {2490507},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
}
@article{sernotavlbl,
 author = {Davidson, Susan B. and Garcia-Molina, Hector and Skeen, Dale},
 title = {{Consistency in a Partitioned Network: A Survey}},
 journal = {ACM Comput. Surv.},
 issue_date = {Sept. 1985},
 volume = {17},
 number = {3},
 month = sep,
 year = {1985},
 issn = {0360-0300},
 pages = {341--370},
 numpages = {30},
 url = {http://doi.acm.org/10.1145/5505.5508},
 doi = {10.1145/5505.5508},
 acmid = {5508},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@inproceedings{bernsigmod13,
 author = {Bernstein, Philip A. and Das, Sudipto},
 title = {{Rethinking Eventual Consistency}},
 booktitle = {Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data},
 series = {SIGMOD '13},
 year = {2013},
 isbn = {978-1-4503-2037-5},
 location = {New York, New York, USA},
 pages = {923--928},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/2463676.2465339},
 doi = {10.1145/2463676.2465339},
 acmid = {2465339},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {eventual consistency, replication},
}
@article{bailisvldb,
 author = {Bailis, Peter and Fekete, Alan and Franklin, Michael J. and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
 title = {{Coordination Avoidance in Database Systems}},
 journal = {Proc. VLDB Endow.},
 issue_date = {November 2014},
 volume = {8},
 number = {3},
 month = nov,
 year = {2014},
 issn = {2150-8097},
 pages = {185--196},
 numpages = {12},
 url = {http://dx.doi.org/10.14778/2735508.2735509},
 doi = {10.14778/2735508.2735509},
 acmid = {2735509},
 publisher = {VLDB Endowment},
}
@inproceedings{bailisferal,
 author = {Bailis, Peter and Fekete, Alan and Franklin, Michael J. and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
 title = {{Feral Concurrency Control: An Empirical Investigation of Modern Application Integrity}},
 booktitle = {Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data},
 series = {SIGMOD '15},
 year = {2015},
 isbn = {978-1-4503-2758-9},
 location = {Melbourne, Victoria, Australia},
 pages = {1327--1342},
 numpages = {16},
 url = {http://doi.acm.org/10.1145/2723372.2737784},
 doi = {10.1145/2723372.2737784},
 acmid = {2737784},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {application integrity, concurrency control, impedance mismatch, invariants, orms, ruby on rails},
}
@inproceedings{gotsmanpopl16,
 author = {Gotsman, Alexey and Yang, Hongseok and Ferreira, Carla and Najafzadeh, Mahsa and Shapiro, Marc},
 title = {{'Cause I'm Strong Enough: Reasoning About Consistency Choices in Distributed Systems}},
 booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL 2016},
 year = {2016},
 isbn = {978-1-4503-3549-2},
 location = {St. Petersburg, FL, USA},
 pages = {371--384},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2837614.2837625},
 doi = {10.1145/2837614.2837625},
 acmid = {2837625},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Replication, causal consistency, integrity invariants},
}
@inproceedings{gotsmanconcur15,
  author =  {Andrea Cerone and Giovanni Bernardi and Alexey Gotsman},
  title = {{A Framework for Transactional Consistency Models with Atomic Visibility}},
  booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages = {58--71},
  series =  {Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =  {978-3-939897-91-0},
  ISSN =  {1868-8969},
  year =  {2015},
  volume =  {42},
  editor =  {Luca Aceto and David de Frutos Escrig},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address = {Dagstuhl, Germany},
  URL =   {http://drops.dagstuhl.de/opus/volltexte/2015/5375},
  URN =   {urn:nbn:de:0030-drops-53756},
  doi =   {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.58},
  annote =  {Keywords: Replication, Consistency models, Transactions}
}
@inproceedings{pldi15,
 author = {Sivaramakrishnan, KC and Kaki, Gowtham and Jagannathan, Suresh},
 title = {{Declarative Programming over Eventually Consistent Data Stores}},
 booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI 2015},
 year = {2015},
 isbn = {978-1-4503-3468-6},
 location = {Portland, OR, USA},
 pages = {413--424},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2737924.2737981},
 doi = {10.1145/2737924.2737981},
 acmid = {2737981},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Availability, Axiomatic Contracts, CRDTs, Cassandra, Contract Classification, Decidable Logic, Distributed Transactions, Eventual Consistency, Haskell, Quelea, SMT solvers},
}
@article{feketevldb09,
 author = {Fekete, Alan and Goldrei, Shirley N. and Asenjo, Jorge P{\'e}rez},
 title = {{Quantifying Isolation Anomalies}},
 journal = {Proc. VLDB Endow.},
 issue_date = {August 2009},
 volume = {2},
 number = {1},
 month = aug,
 year = {2009},
 issn = {2150-8097},
 pages = {467--478},
 numpages = {12},
 url = {http://dx.doi.org/10.14778/1687627.1687681},
 doi = {10.14778/1687627.1687681},
 acmid = {1687681},
 publisher = {VLDB Endowment},
}
@inproceedings{psi,
 author = {Sovran, Yair and Power, Russell and Aguilera, Marcos K. and Li, Jinyang},
 title = {{Transactional Storage for Geo-replicated Systems}},
 booktitle = {Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles},
 series = {SOSP '11},
 year = {2011},
 isbn = {978-1-4503-0977-6},
 location = {Cascais, Portugal},
 pages = {385--400},
 numpages = {16},
 url = {http://doi.acm.org/10.1145/2043556.2043592},
 doi = {10.1145/2043556.2043592},
 acmid = {2043592},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {asynchronous replication, distributed storage, geo-distributed systems, key-value store, parallel snapshot isolation, transactions},
} 
@inproceedings{nmsi,
 author = {Ardekani, Masoud Saeida and Sutra, Pierre and Shapiro, Marc},
 title = {{Non-monotonic Snapshot Isolation: Scalable and Strong Consistency for Geo-replicated Transactional Systems}},
 booktitle = {Proceedings of the 2013 IEEE 32Nd International Symposium on Reliable Distributed Systems},
 series = {SRDS '13},
 year = {2013},
 isbn = {978-0-7695-5115-9},
 pages = {163--172},
 numpages = {10},
 url = {http://dx.doi.org/10.1109/SRDS.2013.25},
 doi = {10.1109/SRDS.2013.25},
 acmid = {2553433},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {Distributed Transactional Systems, Distributed Databases, Partial Replication, Concurrency Control, Multiversioning},
}

@inproceedings{spanner,
 author = {Corbett, James C. and Dean, Jeffrey and Epstein, Michael and Fikes, Andrew and Frost, Christopher and Furman, J. J. and Ghemawat, Sanjay and Gubarev, Andrey and Heiser, Christopher and Hochschild, Peter and Hsieh, Wilson and Kanthak, Sebastian and Kogan, Eugene and Li, Hongyi and Lloyd, Alexander and Melnik, Sergey and Mwaura, David and Nagle, David and Quinlan, Sean and Rao, Rajesh and Rolig, Lindsay and Saito, Yasushi and Szymaniak, Michal and Taylor, Christopher and Wang, Ruth and Woodford, Dale},
 title = {{Spanner: Google's Globally-distributed Database}},
 booktitle = {Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation},
 series = {OSDI'12},
 year = {2012},
 isbn = {978-1-931971-96-6},
 location = {Hollywood, CA, USA},
 pages = {251--264},
 numpages = {14},
 url = {http://dl.acm.org/citation.cfm?id=2387880.2387905},
 acmid = {2387905},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 
@inproceedings{berenson,
	author = {Berenson, Hal and Bernstein, Phil and Gray, Jim and Melton, Jim and O'Neil, Elizabeth and O'Neil, Patrick},
	title = {{A Critique of ANSI SQL Isolation Levels}},
	booktitle = {{Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data}},
	series = {SIGMOD '95},
	year = {1995},
	isbn = {0-89791-731-6},
	location = {San Jose, California, USA},
	pages = {1--10},
	numpages = {10},
	doi = {10.1145/223784.223785},
	acmid = {223785},
	publisher = {ACM},
	address = {New York, NY, USA},
}
@phdthesis{adyaphd,
 author = {Adya, Atul},
 title = {{Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions}},
 year = {1999},
 note = {AAI0800775},
 publisher = {Massachusetts Institute of Technology},
 address = {Cambridge, MA, USA},
}
@phdthesis{zawirski-thesis,
  author={Marek Zawirski},
  title={Dependable Eventual Consistency with Replicated Data Types},
  year = {2015},
}
@misc{zhang,
      title={Remove-Win: a Design Framework for Conflict-free Replicated Data Collections}, 
      author={Yuqi Zhang and Yu Huang and Hengfeng Wei and Jian Lu},
      year={2019},
      eprint={1905.01403},
      archivePrefix={arXiv},
      primaryClass={cs.DC}
}
@article{rga,
	author = {Roh, Hyun-Gul and Jeon, Myeongjae and Kim, Jin-Soo and Lee, Joonwon},
	title = {Replicated Abstract Data Types: Building Blocks for Collaborative Applications},
	year = {2011},
	issue_date = {March, 2011},
	publisher = {Academic Press, Inc.},
	address = {USA},
	volume = {71},
	number = {3},
	issn = {0743-7315},
	url = {https://doi.org/10.1016/j.jpdc.2010.12.006},
	doi = {10.1016/j.jpdc.2010.12.006},
	journal = {J. Parallel Distrib. Comput.},
	month = {mar},
	pages = {354–368},
	numpages = {15},
}
@article{json-crdt,
   title={A Conflict-Free Replicated JSON Datatype},
   volume={28},
   ISSN={1045-9219},
   url={http://dx.doi.org/10.1109/TPDS.2017.2697382},
   DOI={10.1109/tpds.2017.2697382},
   number={10},
   journal={IEEE Transactions on Parallel and Distributed Systems},
   publisher={Institute of Electrical and Electronics Engineers (IEEE)},
   author={Kleppmann, Martin and Beresford, Alastair R.},
   year={2017},
   month={Oct},
   pages={2733–2746}
}

@article{kemmevldb,
 author = {Zellag, Kamal and Kemme, Bettina},
 title = {{Consistency Anomalies in Multi-tier Architectures: Automatic Detection and Prevention}},
 journal = {The VLDB Journal},
 issue_date = {February  2014},
 volume = {23},
 number = {1},
 month = feb,
 year = {2014},
 issn = {1066-8888},
 pages = {147--172},
 numpages = {26},
 doi = {10.1007/s00778-013-0318-x},
 acmid = {2581630},
 publisher = {Springer-Verlag New York, Inc.},
 address = {Secaucus, NJ, USA},
 keywords = {Consistency, Serializability, Transactions},
} 
@inproceedings{feketesigmod08,
 author = {Cahill, Michael J. and R\"{o}hm, Uwe and Fekete, Alan D.},
 title = {{Serializable Isolation for Snapshot Databases}},
 booktitle = {Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data},
 series = {SIGMOD '08},
 year = {2008},
 isbn = {978-1-60558-102-6},
 location = {Vancouver, Canada},
 pages = {729--738},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1376616.1376690},
 doi = {10.1145/1376616.1376690},
 acmid = {1376690},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {multiversion concurrency control, serializability theory, snapshot isolation},
} 
@inproceedings{pssi2011,
 author = {Revilak, Stephen and O'Neil, Patrick and O'Neil, Elizabeth},
 title = {{Precisely Serializable Snapshot Isolation (PSSI)}},
 booktitle = {Proceedings of the 2011 IEEE 27th International Conference on Data Engineering},
 series = {ICDE '11},
 year = {2011},
 isbn = {978-1-4244-8959-6},
 pages = {482--493},
 numpages = {12},
 url = {http://dx.doi.org/10.1109/ICDE.2011.5767853},
 doi = {10.1109/ICDE.2011.5767853},
 acmid = {2005666},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
}
@inproceedings{burckhardt14,
	author = {Burckhardt, Sebastian and Gotsman, Alexey and Yang, Hongseok and Zawirski, Marek},
	title = {{Replicated Data Types: Specification, Verification, Optimality}},
	booktitle = {{Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}},
	series = {POPL '14},
	year = {2014},
	isbn = {978-1-4503-2544-8},
	location = {San Diego, California, USA},
	pages = {271--284},
	numpages = {14},
	doi = {10.1145/2535838.2535848},
	acmid = {2535848},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {eventual consistency, replication, weak memory},
}
@misc{starbucksbug,
	key = {Starbucks Bug},
	title={{Hacking Starbucks for unlimited coffee}},
	url = {http://sakurity.com/blog/2015/05/21/starbucks.html},
	year = {2016}

}
@misc{scimedbug,
	key = {SciMed Bug},
	title={{Avoid Race Conditions that Violate Uniqueness Validation - Rails}},
	url = {http://goo.gl/0QhMQj},
	year = {2016}

}
@misc{poloniexbug,
	key = {Poloniex Bug},
	title={{BTC Stolen from Poloniex}},
	url = {https://bitcointalk.org/index.php?topic=499580},
	year = {2016}

}
@misc{bitcoinbug,
	key = {Bitcoin Bug},
	title={{How I Stole Roughly 100 BTC From an Exchange and How I Could Have Stolen More!}},
	url = {https://goo.gl/4SqaP2},
	year = {2016}

}


@inproceedings{fekete2005,
 author = {Fekete, Alan},
 title = {{Allocating Isolation Levels to Transactions}},
 booktitle = {Proceedings of the Twenty-fourth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems},
 series = {PODS '05},
 year = {2005},
 isbn = {1-59593-062-0},
 location = {Baltimore, Maryland},
 pages = {206--215},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1065167.1065193},
 doi = {10.1145/1065167.1065193},
 acmid = {1065193},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {anomaly, concurrency control, consistency, serializability, snapshot isolation, two-phase locking},
}
@article{feketessi,
 author = {Fekete, Alan and Liarokapis, Dimitrios and O'Neil, Elizabeth and O'Neil, Patrick and Shasha, Dennis},
 title = {{Making Snapshot Isolation Serializable}},
 journal = {ACM Trans. Database Syst.},
 issue_date = {June 2005},
 volume = {30},
 number = {2},
 month = jun,
 year = {2005},
 issn = {0362-5915},
 pages = {492--528},
 numpages = {37},
 url = {http://doi.acm.org/10.1145/1071610.1071615},
 doi = {10.1145/1071610.1071615},
 acmid = {1071615},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Concurrency control, anomaly, consistency, multiversion concurrency, serializability, snapshot isolation, weak isolation},
} 
@inproceedings{bern2000,
 author = {Bernstein, Arthur J. and Lewis, Philip M. and Lu, Shiyong},
 title = {{Semantic Conditions for Correctness at Different Isolation Levels}},
 booktitle = {Proceedings of the 16th International Conference on Data Engineering},
 series = {ICDE '00},
 year = {2000},
 isbn = {0-7695-0506-6},
 pages = {57--},
 url = {http://dl.acm.org/citation.cfm?id=846219.847381},
 acmid = {847381},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {Isolation Levels, Semantic Correctness, Serializability},
key = {{$\!\!$}} ,
}
@inproceedings{battycpp,
 author = {Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark},
 title = {{Mathematizing C++ Concurrency}},
 booktitle = {Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '11},
 year = {2011},
 isbn = {978-1-4503-0490-0},
 location = {Austin, Texas, USA},
 pages = {55--66},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1926385.1926394},
 doi = {10.1145/1926385.1926394},
 acmid = {1926394},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {relaxed memory models, semantics},
} 
@inproceedings{rgtso,
 author = {Ridge, Tom},
 title = {{A Rely-Guarantee Proof System for x86-TSO}},
 booktitle = {Proceedings of the Third International Conference on Verified Software: Theories, Tools, Experiments},
 series = {VSTTE'10},
 year = {2010},
 isbn = {3-642-15056-X, 978-3-642-15056-2},
 location = {Edinburgh, UK},
 pages = {55--70},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=1884866.1884873},
 acmid = {1884873},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}
@inproceedings{rsl13,
 author = {Vafeiadis, Viktor and Narayan, Chinmay},
 title = {{Relaxed Separation Logic: A Program Logic for C11 Concurrency}},
 booktitle = {Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages \&\#38; Applications},
 series = {OOPSLA '13},
 year = {2013},
 isbn = {978-1-4503-2374-1},
 location = {Indianapolis, Indiana, USA},
 pages = {867--884},
 numpages = {18},
 url = {http://doi.acm.org/10.1145/2509136.2509532},
 doi = {10.1145/2509136.2509532},
 acmid = {2509532},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {c/c++, concurrency, proof system, separation logic, weak memory models},
} 
@inproceedings{ferreira10,
 author = {Ferreira, Rodrigo and Feng, Xinyu and Shao, Zhong},
 title = {{Parameterized Memory Models and Concurrent Separation Logic}},
 booktitle = {Proceedings of the 19th European Conference on Programming Languages and Systems},
 series = {ESOP'10},
 year = {2010},
 isbn = {3-642-11956-5, 978-3-642-11956-9},
 location = {Paphos, Cyprus},
 pages = {267--286},
 numpages = {20},
 url = {http://dx.doi.org/10.1007/978-3-642-11957-6_15},
 doi = {10.1007/978-3-642-11957-6_15},
 acmid = {2175501},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}
@article{csl,
 author = {Vafeiadis, Viktor},
 title = {{Concurrent Separation Logic and Operational Semantics}},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {September, 2011},
 volume = {276},
 month = sep,
 year = {2011},
 issn = {1571-0661},
 pages = {335--351},
 numpages = {17},
 url = {http://dx.doi.org/10.1016/j.entcs.2011.09.029},
 doi = {10.1016/j.entcs.2011.09.029},
 acmid = {2048861},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Separation logic, concurrency, race condition, soundness},
}
@inproceedings{linkbench,
 author = {Armstrong, Timothy G. and Ponnekanti, Vamsi and Borthakur, Dhruba and Callaghan, Mark},
 title = {{LinkBench: A Database Benchmark Based on the Facebook Social Graph}},
 booktitle = {Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data},
 series = {SIGMOD '13},
 year = {2013},
 isbn = {978-1-4503-2037-5},
 location = {New York, New York, USA},
 pages = {1185--1196},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2463676.2465296},
 doi = {10.1145/2463676.2465296},
 acmid = {2465296},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {database benchmarks, database workload analysis, hbase, mysql, social networks},
} 
@misc{postgresiso,
	key = {PostgresSQL},
	title={{Transaction Isolation}},
	url = {https://www.postgresql.org/docs/9.1/static/transaction-iso.html},
	note = {Accessed: 2016-07-1 10:00:00},
	year = {2016}
}
@misc{mysqliso,
	key = {MySQL},
	title={{Transaction Isolation Levels}},
	url = {https://dev.mysql.com/doc/refman/5.6/en/innodb-transaction-isolation-levels.html},
	note = {Accessed: 2016-07-1 10:00:00},
	year = {2016}
}
@misc{oracleiso,
	key = {Oracle},
	title={{Data Concurrency and Consistency}},
	url = {https://docs.oracle.com/cd/B28359_01/server.111/b28318/consist.htm},
	note = {Accessed: 2016-07-1 10:00:00},
	year = {2016}
}
@inproceedings{DLZ+13,
 author = {Demange, Delphine and Laporte, Vincent and Zhao, Lei and Jagannathan, Suresh and Pichardie, David and Vitek, Jan},
 title = {{Plan B: A Buffered Memory Model for Java}},
 booktitle = {Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '13},
 year = {2013},
 isbn = {978-1-4503-1832-7},
 location = {Rome, Italy},
 pages = {329--342},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2429069.2429110},
 doi = {10.1145/2429069.2429110},
 acmid = {2429110},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrency, java, memory model, verified compilation},
} 
@article{rgjones,
 author = {Jones, C. B.},
 title = {{Tentative Steps Toward a Development Method for Interfering Programs}},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {Oct. 1983},
 volume = {5},
 number = {4},
 month = oct,
 year = {1983},
 issn = {0164-0925},
 pages = {596--619},
 numpages = {24},
 url = {http://doi.acm.org/10.1145/69575.69577},
 doi = {10.1145/69575.69577},
 acmid = {69577},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@inproceedings{bayou,
 author = {Terry, D. B. and Theimer, M. M. and Petersen, Karin and Demers, A. J. and Spreitzer, M. J. and Hauser, C. H.},
 title = {{Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System}},
 booktitle = {Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles},
 series = {SOSP '95},
 year = {1995},
 isbn = {0-89791-715-4},
 location = {Copper Mountain, Colorado, USA},
 pages = {172--182},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/224056.224070},
 doi = {10.1145/224056.224070},
 acmid = {224070},
 publisher = {ACM},
 address = {New York, NY, USA},
}
@book{railsbook,
 author = {Hartl, Michael},
 title = {{The Ruby On Rails Tutorial}},
 year = {2015},
 isbn = {978-0134077703},
 edition = {3},
 publisher = {Addison-Wesley},
}
@inproceedings{gotsmanpodc16,
 author = {Cerone, Andrea and Gotsman, Alexey},
 title = {{Analysing Snapshot Isolation}},
 booktitle = {Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing},
 series = {PODC},
 year = 2016,
 location = {Chicago, IL},
} 
@article{BG81,
 author = {Bernstein, Philip A. and Goodman, Nathan},
 title = {{Multiversion Concurrency Control - Theory and Algorithms}},
 journal = {ACM Trans. Database Syst.},
 issue_date = {Dec. 1983},
 volume = {8},
 number = {4},
 month = dec,
 year = {1983},
 issn = {0362-5915},
 pages = {465--483},
 numpages = {19},
 url = {http://doi.acm.org/10.1145/319996.319998},
 doi = {10.1145/319996.319998},
 acmid = {319998},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {transaction processing},
} 
@inproceedings{bailisbolton,
	author = {Bailis, Peter and Ghodsi, Ali and Hellerstein, Joseph M. and Stoica, Ion},
	title = {{Bolt-on Causal Consistency}},
	booktitle = {{Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data}},
	series = {SIGMOD '13},
	year = {2013},
	isbn = {978-1-4503-2037-5},
	location = {New York, New York, USA},
	pages = {761--772},
	numpages = {12},
	doi = {10.1145/2463676.2465279},
	acmid = {2465279},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {causal consistency, eventual consistency, separation of concerns},
}

@incollection{crdt,
	author={Shapiro, Marc and Preguiça, Nuno and Baquero, Carlos and Zawirski, Marek},
	year={2011},
	isbn={978-3-642-24549-7},
	booktitle={{Stabilization, Safety, and Security of Distributed Systems}},
	volume={6976},
	series={Lecture Notes in Computer Science},
	editor={Défago, Xavier and Petit, Franck and Villain, Vincent},
	doi={10.1007/978-3-642-24550-3_29},
	title={{Conflict-Free Replicated Data Types}},
	publisher={Springer Berlin Heidelberg},
	keywords={Eventual Consistency; Replicated Shared Objects; Large-Scale Distributed Systems},
	pages={386-400},
	language={English}
}


@inproceedings{GHE15,
 author = {Gammie, Peter and Hosking, Antony L. and Engelhardt, Kai},
 title = {Relaxing Safely: Verified On-the-fly Garbage Collection for x86-TSO},
 booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '15},
 year = {2015},
 isbn = {978-1-4503-3468-6},
 location = {Portland, OR, USA},
 pages = {99--109},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/2737924.2738006},
 doi = {10.1145/2737924.2738006},
 acmid = {2738006},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {TSO, formal verification, machine-checked proof, relaxed memory},
} 


@Inbook{HPQ+15,
author="Hawblitzel, Chris and Petrank, Erez and Qadeer, Shaz and Tasiran, Serdar",
editor="Kroening, Daniel and P{\u{a}}s{\u{a}}reanu, Corina S.",
title= {{Automated and Modular Refinement Reasoning for Concurrent Programs}},
bookTitle="Computer Aided Verification: 27th International Conference",
year="2015",
publisher="Springer International Publishing",
pages="449--465",
isbn="978-3-319-21668-3",
doi="10.1007/978-3-319-21668-3_26",
url="http://dx.doi.org/10.1007/978-3-319-21668-3_26"}

@inproceedings(CPA+17,
  author = {Natacha Crooks and Youer Pu and Lorenzo Alvisi and Allen Clement},
  booktitle = {Proceedings of the ACM Conference on Principles of Distributed Computing},
  year = 2017)

@article{JLP+14,
 author = {Jagannathan, Suresh and Laporte, Vincent and Petri, Gustavo and Pichardie, David and Vitek, Jan},
 title = {Atomicity Refinement for Verified Compilation},
 journal = {SIGPLAN Not.},
 issue_date = {June 2014},
 volume = {49},
 number = {6},
 month = jun,
 year = {2014},
 issn = {0362-1340},
 pages = {27--27},
 numpages = {1},
 url = {http://doi.acm.org/10.1145/2666356.2594346},
 doi = {10.1145/2666356.2594346},
 acmid = {2594346},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@techreport{z3epr,
  author = {Piskac, Ruzica and  de Moura, Leonardo and Bj{\o}rner, Nikolaj},
  title = {{Deciding Effectively Propositional Logic with Equality}},
  number = {MSR-TR-2008-181},
}

@incollection{VP07,
author = {{Vafeiadis, Viktor} and {Parkinson, Matthew}},
title = {{A Marriage of Rely/Guarantee and Separation Logic}},
booktitle = {CONCUR 2007 {\textendash} Concurrency Theory},
year = {2007},
pages = {256--271},
publisher = {Springer Berlin Heidelberg},
address = {Berlin, Heidelberg},
month = sep
}

@inproceedings{Vaf10,
author = {{Vafeiadis, Viktor}},
title = {{RGSep Action Inference}},
booktitle = {Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation},
year = {2010},
pages="345--361",
}

@inproceedings{Vaf10a,
 author = {Vafeiadis, Viktor},
 title = {Automatically Proving Linearizability},
 booktitle = {Proceedings of the 22$^{nd}$ International Conference on Computer Aided Verification},
 series = {CAV'10},
 year = {2010},
 isbn = {3-642-14294-X, 978-3-642-14294-9},
 location = {Edinburgh, UK},
 pages = {450--464},
 numpages = {15},
 url = {http://dx.doi.org/10.1007/978-3-642-14295-6_40},
 doi = {10.1007/978-3-642-14295-6_40},
 acmid = {2144361},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 


@inproceedings{Rey02,
author = {Reynolds, J C},
title = {{Separation Logic: A Logic for Shared Mutable Data Structures}},
booktitle = {17$^{th}$ Annual IEEE Symposium on Logic in Computer Science},
year = {2002},
pages = {55--74},
publisher = {IEEE Comput. Soc}
}

@inproceedings{KJ14,
 author = {Kaki, Gowtham and Jagannathan, Suresh},
 title = {{A Relational Framework for Higher-order Shape Analysis}},
 booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '14},
 year = {2014},
 isbn = {978-1-4503-2873-9},
 location = {Gothenburg, Sweden},
 pages = {311--324},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2628136.2628159},
 doi = {10.1145/2628136.2628159},
 acmid = {2628159},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {decidability, dependent types, inductive relations, parametric relations, relational specifications, standard ml},
} 

@article{eprsla,
  author    = {Matthias Horbach and
               Marco Voigt and
               Christoph Weidenbach},
  title     = {On the Combination of the Bernays-Sch{\"{o}}nfinkel-Ramsey Fragment
               with Simple Linear Integer Arithmetic},
  journal   = {CoRR},
  volume    = {abs/1705.08792},
  year      = {2017},
  url       = {http://arxiv.org/abs/1705.08792},
  timestamp = {Wed, 07 Jun 2017 14:42:14 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/HorbachVW17a},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{terry,
	author = {Terry, Douglas B. and Demers, Alan J. and Petersen, Karin and Spreitzer, Mike and Theimer, Marvin and Welch, Brent W.},
	title = {{Session Guarantees for Weakly Consistent Replicated Data}},
	booktitle = {{Proceedings of the Third International Conference on Parallel and Distributed Information Systems}},
	series = {PDIS '94},
	year = {1994},
	isbn = {0-8186-6400-2},
	pages = {140--149},
	numpages = {10},
	url = {http://dl.acm.org/citation.cfm?id=645792.668302},
	acmid = {668302},
	publisher = {IEEE Computer Society},
	address = {Washington, DC, USA},
}


@inproceedings{DynamoDB,
	author = {Sivasubramanian, Swaminathan},
	title = {{Amazon dynamoDB: A Seamlessly Scalable Non-relational Database Service}},
	booktitle = {{Proceedings of the 2012 ACM SIGMOD International Conference on Management of Data}},
	series = {SIGMOD '12},
	year = {2012},
	isbn = {978-1-4503-1247-9},
	location = {Scottsdale, Arizona, USA},
	pages = {729--730},
	numpages = {2},
	doi = {10.1145/2213836.2213945},
	acmid = {2213945},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {distributed databases, non-relational databases, scalability},
}

@article{Bailis:2013th,
author = {Bailis, P and Ghodsi, A},
title = {{Eventual consistency Today: Limitations, Extensions, and Beyond}},
journal = {Communications of the ACM},
year = {2013}
}

@inproceedings{Alvaro:2013:CWB:2523616.2523632,
 author = {Alvaro, Peter and Bailis, Peter and Conway, Neil and Hellerstein, Joseph M.},
 title = {{Consistency Without Borders}},
 booktitle = {Proceedings of the 4th Annual Symposium on Cloud Computing},
 series = {SOCC '13},
 year = {2013},
 isbn = {978-1-4503-2428-1},
 location = {Santa Clara, California},
 pages = {23:1--23:10},
 articleno = {23},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/2523616.2523632},
 doi = {10.1145/2523616.2523632},
 acmid = {2523632},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article{Sewell:2012ug,
author = {Sewell, P},
title = {{False Concurrency and Strange-but-True Machines}},
journal = {CONCUR 2012},
year = {2012}
}

@inproceedings{BD+17,
 author = {Brutschy, Lucas and Dimitrov, Dimitar and M\"{u}ller, Peter and Vechev, Martin},
 title = {Serializability for Eventual Consistency: Criterion, Analysis, and Applications},
 booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 series = {POPL 2017},
 year = {2017},
 isbn = {978-1-4503-4660-3},
 location = {Paris, France},
 pages = {458--472},
 numpages = {15},
 url = {http://doi.acm.org/10.1145/3009837.3009895},
 doi = {10.1145/3009837.3009895},
 acmid = {3009895},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Replication, eventual consistency, serializability},
} 


@misc{tpc,
  key = {TPC},
  note = "TPC Benchmarks",
  url = "http://www.tpc.org/information/benchmarks.asp",
  year = 2018
}

@misc{riak,
  key = {Riak},
  note = "Riak NoSQL Database",
  url = "docs.basho.com/riak/kv/2.2.3/",
  year = 2018
}

@misc{antidote,
   author = {{Shapiro}, M. and {Bieniusa}, A. and {Pregui{\c c}a}, N. and 
	{Balegas}, V. and {Meiklejohn}, C.},
    title = {{Just-Right Consistency: Reconciling Availability and Safety}},
  note = {ArXiv e-prints},
     year = 2018,
    month = jan,
   adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180106340S},
}

@inproceedings{BM10,
author="Burckhardt, Sebastian and Musuvathi, Madanlal and Singh, Vasu",
editor="Gupta, Rajiv",
title="Verifying Local Transformations on Relaxed Memory Models",
booktitle="Compiler Construction",
year="2010",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="104--123",
isbn="978-3-642-11970-5"
}

@article{Moggi91,
 author = {Moggi, Eugenio},
 title = {Notions of Computation and Monads},
 journal = {Inf. Comput.},
 issue_date = {July 1991},
 volume = {93},
 number = {1},
 month = jul,
 year = {1991},
 issn = {0890-5401},
 pages = {55--92},
 numpages = {38},
 url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
 doi = {10.1016/0890-5401(91)90052-4},
 acmid = {116984},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
} 

@misc{voldemort,
 key = {Voldemort},
 year = "",
 note = {Voldemort Distributed Database},
 url = {http://www.project-voldemort.com/voldemort/design.html}
}

@inproceedings{heap-epr,
 author = {Itzhaky, Shachar and Banerjee, Anindya and Immerman, Neil and Lahav, Ori and Nanevski, Aleksandar and Sagiv, Mooly},
 title = {Modular Reasoning About Heap Paths via Effectively Propositional Formulas},
 booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '14},
 year = {2014},
 isbn = {978-1-4503-2544-8},
 location = {San Diego, California, USA},
 pages = {385--396},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2535838.2535854},
 doi = {10.1145/2535838.2535854},
 acmid = {2535854},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {linked list, smt, verification},
} 


@article{BVF+12,
 author = {Bailis, Peter and Venkataraman, Shivaram and Franklin, Michael J. and Hellerstein, Joseph M. and Stoica, Ion},
 title = {{Probabilistically Bounded Staleness for Practical Partial Quorums}},
 journal = {Proc. VLDB Endow.},
 issue_date = {April 2012},
 volume = {5},
 number = {8},
 month = apr,
 year = {2012},
 issn = {2150-8097},
 pages = {776--787},
 numpages = {12},
 url = {http://dx.doi.org/10.14778/2212351.2212359},
 doi = {10.14778/2212351.2212359},
 acmid = {2212359},
 publisher = {VLDB Endowment},
} 


@article{KN+18,
 author = {Kaki, Gowtham and Nagar, Kartik and Najafzadeh, Mahsa and Jagannathan, Suresh},
 title = {Alone Together: Compositional Reasoning and Inference for Weak Isolation},
 journal = {Proc. ACM Program. Lang.},
 issue_date = {January 2018},
 volume = {2},
 number = {POPL},
 month = dec,
 year = {2017},
 issn = {2475-1421},
 pages = {27:1--27:34},
 articleno = {27},
 numpages = {34},
 url = {http://doi.acm.org/10.1145/3158115},
 doi = {10.1145/3158115},
 acmid = {3158115},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Concurrency, Rely-Guarantee, Transactions, Verification, Weak Isolation},
} 


@inproceedings{AM+10,
 author = {Alglave, Jade and Maranget, Luc and Sarkar, Susmit and Sewell, Peter},
 title = {{Fences in Weak Memory Models}} ,
 booktitle = {Proceedings of the 22Nd International Conference on Computer Aided Verification},
 series = {CAV'10},
 year = {2010},
 isbn = {3-642-14294-X, 978-3-642-14294-9},
 location = {Edinburgh, UK},
 pages = {258--272},
 numpages = {15},
 url = {http://dx.doi.org/10.1007/978-3-642-14295-6_25},
 doi = {10.1007/978-3-642-14295-6_25},
 acmid = {2144342},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 

@inproceedings{BT17,
 author = {Bornholt, James and Torlak, Emina},
 title = {Synthesizing Memory Models from Framework Sketches and Litmus Tests},
 booktitle = {Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI 2017},
 year = {2017},
 isbn = {978-1-4503-4988-8},
 location = {Barcelona, Spain},
 pages = {467--481},
 numpages = {15},
 url = {http://doi.acm.org/10.1145/3062341.3062353},
 doi = {10.1145/3062341.3062353},
 acmid = {3062353},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {program synthesis, weak memory models},
} 

@inproceedings{KA+07,
 author = {Killian, Charles and Anderson, James W. and Jhala, Ranjit and Vahdat, Amin},
 title = {Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code},
 booktitle = {Proceedings of the 4th USENIX Conference on Networked Systems Design \&\#38; Implementation},
 series = {NSDI'07},
 year = {2007},
 location = {Cambridge, MA},
 pages = {18--18},
 numpages = {1},
 url = {http://dl.acm.org/citation.cfm?id=1973430.1973448},
 acmid = {1973448},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 

@article{CS13,
 author = {Cadar, Cristian and Sen, Koushik},
 title = {Symbolic Execution for Software Testing: Three Decades Later},
 journal = {Commun. ACM},
 issue_date = {February 2013},
 volume = {56},
 number = {2},
 month = feb,
 year = {2013},
 issn = {0001-0782},
 pages = {82--90},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/2408776.2408795},
 doi = {10.1145/2408776.2408795},
 acmid = {2408795},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@misc(Jepsen,
 key = {Jepsen},
 url = {https://jepsen.io/},
 year = 2018)

@inproceedings{musuvathi07,
 author = {Musuvathi, Madanlal and Qadeer, Shaz},
 title = {Iterative Context Bounding for Systematic Testing of Multithreaded Programs},
 booktitle = {Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '07},
 year = {2007},
 isbn = {978-1-59593-633-2},
 location = {San Diego, California, USA},
 pages = {446--455},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1250734.1250785},
 doi = {10.1145/1250734.1250785},
 acmid = {1250785},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrency, context-bounding, model checking, multithreading, partial-order reduction, shared-memory programs, software testing},
} 

@inproceedings{musuvathi08,
 author = {Musuvathi, Madanlal and Qadeer, Shaz and Ball, Thomas and Basler, Gerard and Nainar, Piramanayagam Arumuga and Neamtiu, Iulian},
 title = {Finding and Reproducing Heisenbugs in Concurrent Programs},
 booktitle = {Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation},
 series = {OSDI'08},
 year = {2008},
 location = {San Diego, California},
 pages = {267--280},
 numpages = {14},
 url = {http://dl.acm.org/citation.cfm?id=1855741.1855760},
 acmid = {1855760},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 

@article{apostate,
 author = {Helland, Pat},
 title = {Life Beyond Distributed Transactions},
 journal = {Commun. ACM},
 issue_date = {February 2017},
 volume = {60},
 number = {2},
 month = jan,
 year = {2017},
 issn = {0001-0782},
 pages = {46--54},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/3009826},
 doi = {10.1145/3009826},
 acmid = {3009826},
 publisher = {ACM},
 address = {New York, NY, USA},
} 
@misc{brewer2013,
 key = {Brewer},
 year = 2013,
 note = {Myth: Eric Brewer on Why Banks are BASE Not ACID - 
   Availability Is Revenue},
 url = {http://highscalability.com/blog/2013/5/1/myth-eric-brewer-on-why-banks-are-base-not-acid-availability.html}
}

@inproceedings{CrooksSigmod16,
 author = {Crooks, Natacha and Pu, Youer and Estrada, Nancy and Gupta, Trinabh and Alvisi, Lorenzo and Clement, Allen},
 title = {TARDiS: A Branch-and-Merge Approach To Weak Consistency},
 booktitle = {Proceedings of the 2016 International Conference on Management of Data},
 series = {SIGMOD '16},
 year = {2016},
 isbn = {978-1-4503-3531-7},
 location = {San Francisco, California, USA},
 pages = {1615--1628},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2882903.2882951},
 doi = {10.1145/2882903.2882951},
 acmid = {2882951},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {causal consistency, databases, distributed systems, eventual consistency, geo-distribution, merging, replication, transactions, weak consistency},
} 

@article{HL19,
  author    = {Farzin Houshmand and
               Mohsen Lesani},
  title     = {{Hamsaz: Replication Coordination Analysis and Synthesis}},
  journal   = {{PACMPL}},
  volume    = {3},
  number    = {{POPL}},
  pages     = {74:1--74:32},
  year      = {2019},
  url       = {https://dl.acm.org/citation.cfm?id=3290387},
  timestamp = {Tue, 22 Jan 2019 15:27:56 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/pacmpl/HoushmandL19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
},

@book{okasaki,
 author = {Okasaki, Chris},
 title = {Purely Functional Data Structures},
 year = {1998},
 isbn = {0-521-63124-6},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
},

@article{Kahr2001,
 author = {Kahrs, Stefan},
 title = {Red-black Trees with Types},
 journal = {J. Funct. Program.},
 issue_date = {July 2001},
 volume = {11},
 number = {4},
 month = jul,
 year = {2001},
 issn = {0956-7968},
 pages = {425--432},
 numpages = {8},
 url = {http://dx.doi.org/10.1017/S0956796801004026},
 doi = {10.1017/S0956796801004026},
 acmid = {968482},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
},

@article{Erwig2001,
 author = {Erwig, Martin},
 title = {Inductive Graphs and Functional Graph Algorithms},
 journal = {J. Funct. Program.},
 issue_date = {September 2001},
 volume = {11},
 number = {5},
 month = sep,
 year = {2001},
 issn = {0956-7968},
 pages = {467--492},
 numpages = {26},
 url = {http://dx.doi.org/10.1017/S0956796801004075},
 doi = {10.1017/S0956796801004075},
 acmid = {968437},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
},

@misc{fgl,
	key = {Functional Graph},
	title={{A Functional Graph Library}},
	url = {http://hackage.haskell.org/package/fgl},
	year = {2008},
},
	
@article{boehm95,
 author = {Boehm, Hans-J. and Atkinson, Russ and Plass, Michael},
 title = {Ropes: An Alternative to Strings},
 journal = {Softw. Pract. Exper.},
 issue_date = {Dec. 1995},
 volume = {25},
 number = {12},
 month = dec,
 year = {1995},
 issn = {0038-0644},
 pages = {1315--1330},
 numpages = {16},
 url = {http://dx.doi.org/10.1002/spe.4380251203},
 doi = {10.1002/spe.4380251203},
 acmid = {219565},
 publisher = {John Wiley \& Sons, Inc.},
 address = {New York, NY, USA},
 keywords = {C, balanced trees, cedar, character strings, concatenation, immutable},
},

@inproceedings{treedoc,
 author = {Preguica, Nuno and Marques, Joan Manuel and Shapiro, Marc and Letia, Mihai},
 title = {A Commutative Replicated Data Type for Cooperative Editing},
 booktitle = {Proceedings of the 2009 29th IEEE International Conference on Distributed Computing Systems},
 series = {ICDCS '09},
 year = {2009},
 isbn = {978-0-7695-3659-0},
 pages = {395--403},
 numpages = {9},
 url = {https://doi.org/10.1109/ICDCS.2009.20},
 doi = {10.1109/ICDCS.2009.20},
 acmid = {1584604},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {commutative replicated data type, distributed algorithms, replicated data, co-operative editing, dense identifier space},
} ,


@misc{AmazonSQS,
  key = {Amazon SQS},
  note = {Amazon Simple Queue Service},
  url = {https://aws.amazon.com/sqs}}


@inproceedings(DP17,
  author = {Stephen Dolan and Mindy Preston},
  title = {{Testing with Crowbar}},
  booktitle = {Proceedings of the OCaml Workshop},
  year = 2017)

@article{jlrs,
 author = {Jeannet, Bertrand and Loginov, Alexey and Reps, Thomas and Sagiv, Mooly},
 title = {A Relational Approach to Interprocedural Shape Analysis},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {January 2010},
 volume = {32},
 number = {2},
 month = feb,
 year = {2010},
 issn = {0164-0925},
 pages = {5:1--5:52},
 articleno = {5},
 numpages = {52},
 url = {http://doi.acm.org/10.1145/1667048.1667050},
 doi = {10.1145/1667048.1667050},
 acmid = {1667050},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {3-valued logic, Abstract interpretation, context-sensitive analysis, destructive updating, interprocedural dataflow analysis, pointer analysis, shape analysis, static analysis},
} 

@inproceedings{Chang2008,
 author = {Chang, Bor-Yuh Evan and Rival, Xavier},
 title = {Relational Inductive Shape Analysis},
 booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '08},
 year = {2008},
 isbn = {978-1-59593-689-9},
 location = {San Francisco, California, USA},
 pages = {247--260},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/1328438.1328469},
 doi = {10.1145/1328438.1328469},
 acmid = {1328469},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {heap analysis, inductive definitions, materialization, separation logic, shape analysis, symbolic abstract domain},
} 

@incollection{Datalog,
 author = {Maier, David and Tekle, K. Tuncay and Kifer, Michael and Warren, David S.},
 chapter = {Datalog: Concepts, History, and Outlook},
 title = {Declarative Logic Programming},
 editor = {Kifer, Michael and Liu, Yanhong Annie},
 year = {2018},
 isbn = {978-1-97000-199-0},
 pages = {3--100},
 numpages = {98},
 url = {https://doi.org/10.1145/3191315.3191317},
 doi = {10.1145/3191315.3191317},
 acmid = {3191317},
 publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool},
 address = {New York, NY, USA},
} 

@inproceedings{Prolog,
 author = {Bowen, Kenneth A.},
 title = {Prolog},
 booktitle = {Proceedings of the 1979 Annual Conference},
 series = {ACM '79},
 year = {1979},
 isbn = {0-89791-008-7},
 pages = {14--23},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/800177.810020},
 doi = {10.1145/800177.810020},
 acmid = {810020},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@InProceedings{carmot,
  author =	{Gowtham Kaki and KC Sivaramakrishnan and Suresh Jagannathan},
  title =	{{Version Control Is for Your Data Too}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Benjamin S. Lerner and Rastislav Bod{\'i}k and Shriram Krishnamurthi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10551},
  URN =		{urn:nbn:de:0030-drops-105516},
  doi =		{10.4230/LIPIcs.SNAPL.2019.8},
  annote =	{Keywords: replication, distributed systems, version control}
}

@article{kleppmann2017,
	author = {Gomes, Victor B. F. and Kleppmann, Martin and Mulligan, Dominic P. and Beresford, Alastair R.},
	title = {Verifying Strong Eventual Consistency in Distributed Systems},
	year = {2017},
	issue_date = {October 2017},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {1},
	number = {OOPSLA},
	url = {https://doi.org/10.1145/3133933},
	doi = {10.1145/3133933},
	journal = {Proc. ACM Program. Lang.},
	month = {oct},
	articleno = {109},
	numpages = {28},
}

@article{mrdt,
	author = {Kaki, Gowtham and Priya, Swarn and Sivaramakrishnan, KC and Jagannathan, Suresh},
	title = {Mergeable Replicated Data Types},
	year = {2019},
	issue_date = {October 2019},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {3},
	number = {OOPSLA},
	url = {https://doi.org/10.1145/3360580},
	doi = {10.1145/3360580},
	journal = {Proc. ACM Program. Lang.},
	month = {oct},
	articleno = {154},
	numpages = {29},
}

@InProceedings{ivy,
	author="McMillan, Kenneth L.
	and Padon, Oded",
	editor="Lahiri, Shuvendu K.
	and Wang, Chao",
	title="Ivy: A Multi-modal Verification Tool for Distributed Algorithms",
	booktitle="Computer Aided Verification",
	year="2020",
	publisher="Springer International Publishing",
	address="Cham",
	pages="190--202",
	isbn="978-3-030-53291-8"
}

@misc{scylla,
	key = {Scylla},
	title={{A Real-Time Big Data Database}},
	url = {https://www.scylladb.com/},
	note = {Accessed: 2021-11-18 13:21:00},
	year = {2021}
}

@article{vectorclock,
	author = {Lamport, Leslie},
	title = {Time, Clocks, and the Ordering of Events in a Distributed System},
	year = {1978},
	issue_date = {July 1978},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {21},
	number = {7},
	issn = {0001-0782},
	url = {https://doi.org/10.1145/359545.359563},
	doi = {10.1145/359545.359563},
	journal = {Commun. ACM},
	month = {jul},
	pages = {558–565},
	numpages = {8},
}
@misc{gnudiff,
	key = {GNU Diffutils},
	title={{GNU Diffutils}},
	url = {https://www.gnu.org/software/diffutils/},
	note = {Accessed: 2021-11-18 13:21:00},
	year = {2021}
}
@misc{canterbury,
	key = {Canterbury},
	title={{The Canterbury Corpus}},
	url = {https://corpus.canterbury.ac.nz/descriptions/},
	note = {Accessed: 2021-11-18 13:21:00},
	year = {2021}
}

@InProceedings{sledge,
author="Blanchette, Jasmin Christian
and B{\"o}hme, Sascha
and Paulson, Lawrence C.",
editor="Bj{\o}rner, Nikolaj
and Sofronie-Stokkermans, Viorica",
title="Extending Sledgehammer with SMT Solvers",
booktitle="Automated Deduction -- CADE-23",
year="2011",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="116--130",
isbn="978-3-642-22438-6"
}

@article{WF92,
author = {Wright, A.K. and Felleisen, M.},
title = {A Syntactic Approach to Type Soundness},
year = {1994},
issue_date = {Nov. 15, 1994},
publisher = {Academic Press, Inc.},
address = {USA},
volume = {115},
number = {1},
issn = {0890-5401},
url = {https://doi.org/10.1006/inco.1994.1093},
doi = {10.1006/inco.1994.1093},
journal = {Inf. Comput.},
month = {nov},
pages = {38–94},
numpages = {57}
}

@inproceedings{Honda96,
author = {Honda, Kohei},
title = {Composing Processes},
year = {1996},
isbn = {0897917693},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/237721.237802},
doi = {10.1145/237721.237802},
booktitle = {Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {344–357},
numpages = {14},
location = {St. Petersburg Beach, Florida, USA},
series = {POPL '96}
}

@misc{tycon,
	key = {Tycon Blog},
	title={{Vagaries of Git Merge}},
	url = {http://tycon.github.io/git-inconsistencies.html},
  note = {Accessed: 2022-03-03 12:21:00},
  year = {2019}
}

@misc{russell,
	key = {Russell O'Connor's Blog},
	title={{Git is Inconsistent}},
	url = {http://r6.ca/blog/20110416T204742Z.html},
  note = {Accessed: 2022-03-19 12:21:00},
  year = {2011}
}

@article{HNMSession16,
author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
title = {Multiparty Asynchronous Session Types},
year = {2016},
issue_date = {March 2016},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {63},
number = {1},
issn = {0004-5411},
url = {https://doi.org/10.1145/2827695},
doi = {10.1145/2827695},
journal = {J. ACM},
month = {mar},
articleno = {9},
numpages = {67},
keywords = {Session types, the pi-calculus, projection, progress, global types, global protocols}
}