--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex Mon Jul 10 14:32:48 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex Mon Jul 10 19:29:22 2023 +0100
@@ -545,22 +545,71 @@
%----------------------------------------------------------------------------------------
\section{Contribution}
-{\color{red} \rule{\linewidth}{0.5mm}}
-\textbf{issue with this part: way too short, not enough details of what I have done.}
-{\color{red} \rule{\linewidth}{0.5mm}}
+%{\color{red} \rule{\linewidth}{0.5mm}}
+%\textbf{issue with this part: way too short, not enough details of what I have done.}
+ %{\color{red} \rule{\linewidth}{0.5mm}}
+\marginpar{\em Gerog: No sufficient context on related work making contribution hard to digest.}
+
-In this thesis,
-we propose a solution to catastrophic
-backtracking and error-prone matchers: a formally verified
-regular expression lexing algorithm
-that is both fast
-and correct.
-{\color{red} \rule{\linewidth}{0.5mm}}
-\HandRight Added content:
+%In this thesis,
+%we propose a solution to catastrophic
+%backtracking and error-prone matchers: a formally verified
+%regular expression lexing algorithm
+%that is both fast
+%and correct.
+%%{\color{red} \rule{\linewidth}{0.5mm}}
+%\HandRight Added content:
%Package \verb`pifont`: \ding{43}
%Package \verb`utfsym`: \usym{261E}
%Package \verb`dingbat`: \leftpointright
%Package \verb`dingbat`: \rightpointright
+We have made mainly two contributions in this thesis: %the
+%lexer we developed based on Brzozowski derivatives and
+%Sulzmanna and Lu's developments called
+proving the lexer $\blexersimp$ is both correctness and fast.
+It is correct w.r.t a formalisation of POSIX lexing by Ausaf et al.\ref{AusafDyckhoffUrban2016}.
+It is fast compared with un-optimised implementations like Sulzmann and Lu's orignal
+development by our metric of internal data structures not growing unbounded.
+
+Our formalisation of complexity is unique among similar works in the sense that
+%is about the size of internal data structures.
+to our knowledge %we don't know of a
+there is not a lexing/parsing algorithm with similar formalised correctness theorems.
+Common practices involve making some empirical analysis of the complexity of the algorithm
+in question (\ref{Verbatim}, \ref{Verbatimpp}), or relying
+on prior (unformalised) complexity analysis of well-known algorithms (\ref{ValiantParsing}),
+making them prone to complexity bugs.
+%TODO: add citation
+%, for example in the Verbatim work \ref{Verbatim}
+
+%While formalised proofs have not included
+%Issues known as "performance bugs" can
+Whilst formalised complexity theorems
+have not yet appeared in other certified lexers/parsers,
+%while this work is done,
+they do find themselves in the broader theorem-proving literature:
+\emph{time credits} have been formalised for separation logic in Coq
+\ref{atkey2010amortised}%not used in
+to characterise the runtime complexity of an algorithm,
+where integer values are recorded %from the beginning of an execution
+as part of the program state
+and decremented in each step.
+The idea is that the total number of decrements
+from the time credits during execution represents the complexity of an algorithm.
+%each time a basic step is executed.
+%The way to use a time credit Time credit is an integer
+%is assigned to a program prior to execution, and each step in the program consumes
+%one credit.
+This has been further developed to include the big-O notation
+so one can prove both the functional correctness and asymptotic complexity
+of higher-order imperative algorithms \ref{bigOImperative}.
+%for example the complexity of
+%the Quicksort algorithm
+%is $\Theta n\ln n$
+
+\marginpar{more work on formalising complexity}.
+\marginpar{new changes up to this point.}
+
In particular, the main problem we solved on top of previous work was
coming up with a formally verified algorithm called $\blexersimp$ based
--- 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}
+%}
+
+