--- a/ChengsongTanPhdThesis/Chapters/Future.tex Fri Jul 14 00:32:41 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Future.tex Mon Jul 24 11:09:48 2023 +0100
@@ -175,6 +175,12 @@
which generates high performance code with proofs
that can be broken down into small steps.
+Extending the Sulzmann and Lu's algorithm to parse
+more pcre regex constructs like lookahead, capture groups
+and back-references with proofs on basic properties like correctness
+seems useful, despite it cannot be made efficient.
+Creating a correct and easy-to-prove version of $\blexersimp$
+seems an appealing next-step for both practice and theory.