-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathreferences.bib
128 lines (121 loc) · 9.22 KB
/
references.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
@misc{Wiki:Differential-Privacy,
author = "Wikipedia",
title = "{Differential privacy} --- {W}ikipedia{,} The Free Encyclopedia",
year = "2024",
howpublished = {\url{http://en.wikipedia.org/w/index.php?title=Differential\%20privacy&oldid=1212542457}},
note = "[Online; accessed 16-May-2024]"
}
@book{Paper:Optimal-Impl-FP,
author = {Asperti, Andrea and Guerrini, Stefano},
title = {The optimal implementation of functional programming languages},
year = {1999},
isbn = {0521621127},
publisher = {Cambridge University Press},
address = {USA}
}
@inproceedings{Paper:Paxos,
title={Paxos Made Simple},
author={Leslie Lamport},
year={2001},
url={https://api.semanticscholar.org/CorpusID:1936192}
}
@inproceedings{Paper:Raft,
author = {Ongaro, Diego and Ousterhout, John},
title = {In search of an understandable consensus algorithm},
year = {2014},
isbn = {9781931971102},
publisher = {USENIX Association},
address = {USA},
abstract = {Raft is a consensus algorithm for managing a replicated log. It produces a result equivalent to (multi-)Paxos, and it is as efficient as Paxos, but its structure is different from Paxos; this makes Raft more understandable than Paxos and also provides a better foundation for building practical systems. In order to enhance understandability, Raft separates the key elements of consensus, such as leader election, log replication, and safety, and it enforces a stronger degree of coherency to reduce the number of states that must be considered. Results from a user study demonstrate that Raft is easier for students to learn than Paxos. Raft also includes a new mechanism for changing the cluster membership, which uses overlapping majorities to guarantee safety.},
booktitle = {Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference},
pages = {305-320},
numpages = {16},
location = {Philadelphia, PA},
series = {USENIX ATC'14}
}
@inproceedings{Paper:Agda-Categories,
author = {Hu, Jason Z. S. and Carette, Jacques},
title = {Formalizing Category Theory in Agda},
year = {2021},
isbn = {9781450382991},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3437992.3439922},
doi = {10.1145/3437992.3439922},
abstract = {The generality and pervasiveness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.},
booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {327–342},
numpages = {16},
keywords = {formal mathematics, Agda, category theory},
location = {Virtual, Denmark},
series = {CPP 2021}
}
@online{Meme:Abstract-Nonsense,
title = {Abstract Nonsense (アブストラクト・ナンセンス) feat. Kagamine Rin},
date = {2015},
organization = {Youtube},
author = {Neru, Kagamine Rin},
url = {https://youtu.be/EjSvChCF9_M?si=Y8qVbM3MeSWucDux},
}
@book{Book:PFPL,
author = {Harper, Robert},
title = {Practical Foundations for Programming Languages},
year = {2016},
isbn = {1107150302},
publisher = {Cambridge University Press},
address = {USA},
edition = {2nd},
abstract = {This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics. Language concepts are precisely defined by their static and dynamic semantics, presenting the essential tools both intuitively and rigorously while relying on only elementary mathematics. These tools are used to analyze and prove properties of languages and provide the framework for combining and comparing language features. The broad range of concepts includes fundamental data types such as sums and products, polymorphic and abstract types, dynamic typing, dynamic dispatch, subtyping and refinement types, symbols and dynamic classification, parallelism and cost semantics, and concurrency and distribution. The methods are directly applicable to language implementation, to the development of logics for reasoning about programs, and to the formal verification language properties such as type safety. This thoroughly revised second edition includes exercises at the end of nearly every chapter and a new chapter on type refinements.}
}
@book{Book:Tiger-Compiler,
author = {Appel, Andrew W. and Ginsburg, Maia},
title = {Modern Compiler Implementation in C},
year = {1998},
isbn = {052158390X},
publisher = {Press Syndicate of the University of Cambridge},
abstract = {From the Publisher:This textbook describes all phases of a modern compiler: lexical analysis, parsing, abstract syntax, semantic actions, intermediate representations, instruction selection via tree matching, dataflow analysis, graph-coloring register allocation, and runtime systems. It includes good coverage of current techniques in code generation and register allocation, as well as functional and object-oriented languages, that is missing from most books. The most accepted and successful techniques are described in a concise way, rather than as an exhaustive catalog of every possible variant. Detailed descriptions of the interfaces between modules of a compiler are illustrated with actual C header files. A unique feature of the book is a well designed compiler implementation project in C, including front-end and "high-tech" back-end phases, so that students can build a complete working compiler in one semester.}
}
@article{Paper:OCC,
author = {Kung, H. T. and Robinson, John T.},
title = {On optimistic methods for concurrency control},
year = {1981},
issue_date = {June 1981},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {2},
issn = {0362-5915},
url = {https://doi.org/10.1145/319566.319567},
doi = {10.1145/319566.319567},
abstract = {Most current approaches to concurrency control in database systems rely on locking of data objects as a control mechanism. In this paper, two families of nonlocking concurrency controls are presented. The methods used are “optimistic” in the sense that they rely mainly on transaction backup as a control mechanism, “hoping” that conflicts between transactions will not occur. Applications for which these methods should be more efficient than locking are discussed.},
journal = {ACM Trans. Database Syst.},
month = {jun},
pages = {213–226},
numpages = {14},
keywords = {concurrency controls, databases, transaction processing}
}
@article{Paper:Spectrum,
author = {Zhihao Chen, and Tianji Yang, Yixiao Zheng, Zhao Zhang, Cheqing Jin, Aoying Zhou},
title = {Spectrum: Speedy and Strictly-Deterministic Smart Contract Transactions for Blockchain Ledgers},
year = {2024},
journal = {PVLDB},
pages = {2541-2554},
volume = {17}
}
@article{Paper:Aria-DCC,
author = {Lu, Yi and Yu, Xiangyao and Cao, Lei and Madden, Samuel},
title = {Aria: a fast and practical deterministic OLTP database},
year = {2020},
issue_date = {August 2020},
publisher = {VLDB Endowment},
volume = {13},
number = {12},
issn = {2150-8097},
url = {https://doi.org/10.14778/3407790.3407808},
doi = {10.14778/3407790.3407808},
abstract = {Deterministic databases are able to efficiently run transactions across different replicas without coordination. However, existing state-of-the-art deterministic databases require that transaction read/write sets are known before execution, making such systems impractical in many OLTP applications. In this paper, we present Aria, a new distributed and deterministic OLTP database that does not have this limitation. The key idea behind Aria is that it first executes a batch of transactions against the same database snapshot in an execution phase, and then deterministically (without communication between replicas) chooses those that should commit to ensure serializability in a commit phase. We also propose a novel deterministic reordering mechanism that allows Aria to order transactions in a way that reduces the number of conflicts. Our experiments on a cluster of eight nodes show that Aria outperforms systems with conventional nondeterministic concurrency control algorithms and the state-of-the-art deterministic databases by up to a factor of two on two popular benchmarks (YCSB and TPC-C).},
journal = {Proc. VLDB Endow.},
month = {jul},
pages = {2047–2060},
numpages = {14}
}