--- a/ChengsongTanPhdThesis/example.bib	Mon Jul 10 14:32:48 2023 +0100
+++ b/ChengsongTanPhdThesis/example.bib	Mon Jul 10 19:29:22 2023 +0100
@@ -1027,3 +1027,69 @@
 	title = {GO regexp package documentation},
 	url = {https://pkg.go.dev/regexp#pkg-overview}
 }
+
+
+@inproceedings{atkey2010amortised,
+  title={Amortised resource analysis with separation logic},
+  author={Atkey, Robert},
+  booktitle={European Symposium on Programming},
+  pages={85--103},
+  year={2010},
+  organization={Springer}
+}
+
+%10.1007/978-3-319-89884-1_19,
+
+@InProceedings{bigOImperative, 
+author="Gu{\'e}neau, Arma{\"e}l
+and Chargu{\'e}raud, Arthur
+and Pottier, Fran{\c{c}}ois",
+editor="Ahmed, Amal",
+title="A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification",
+booktitle="Programming Languages and Systems",
+year="2018",
+publisher="Springer International Publishing",
+address="Cham",
+pages="533--560",
+abstract="We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.",
+isbn="978-3-319-89884-1"
+}
+%@article{10.1145/640128.604148,
+%author = {Hofmann, Martin and Jost, Steffen},
+%title = {Static Prediction of Heap Space Usage for First-Order Functional Programs},
+%year = {2003},
+%issue_date = {January 2003},
+%publisher = {Association for Computing Machinery},
+%address = {New York, NY, USA},
+%volume = {38},
+%number = {1},
+%issn = {0362-1340},
+%url = {https://doi.org/10.1145/640128.604148},
+%doi = {10.1145/640128.604148},
+%abstract = {We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs.The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort.The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system.We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.},
+%journal = {SIGPLAN Not.},
+%month = {jan},
+%pages = {185–197},
+%numpages = {13},
+%keywords = {heap, functional programming, program analysis, resources, garbage collection}
+%}
+%
+%@inproceedings{10.1145/604131.604148,
+%author = {Hofmann, Martin and Jost, Steffen},
+%title = {Static Prediction of Heap Space Usage for First-Order Functional Programs},
+%year = {2003},
+%isbn = {1581136285},
+%publisher = {Association for Computing Machinery},
+%address = {New York, NY, USA},
+%url = {https://doi.org/10.1145/604131.604148},
+%doi = {10.1145/604131.604148},
+%abstract = {We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs.The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort.The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system.We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.},
+%booktitle = {Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+%pages = {185–197},
+%numpages = {13},
+%keywords = {resources, heap, garbage collection, program analysis, functional programming},
+%location = {New Orleans, Louisiana, USA},
+%series = {POPL '03}
+%}
+
+