--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Fahad/results.tex	Fri Aug 25 15:05:20 2017 +0200
@@ -0,0 +1,59 @@
+\documentclass[11pt]{article}
+\usepackage{times}
+\usepackage{amsmath}
+\usepackage{amssymb}
+
+\begin{document}
+
+\noindent
+{\LARGE\bf Fahad's results for thesis}\bigskip
+
+\noindent
+Part 1 (regular expressions)
+
+\begin{itemize}
+\item he corrected the paper by Sulzmann and Lu by giving a new definition
+  for POSIX matching---his proof is completely different than the one
+  by Sulzmann and Lu and formalised in Isabelle
+  
+\item he extended the results by Sulzmann and Lu to all regular
+  expression constructors, excluding back references; to deal with
+  backreferences is probably too difficult for the remaining time
+
+\item he formalised in Isabelle the definition of POSIX matching by Okui and
+  Suzuki and showed that it is equivalent to his definition (his
+  definition is declarative, whereas the one by Okui \& Suzuki is by a
+  position caluculus---so both definitions are quite different
+  technically, but the result is that they define the same `thing')
+
+\item from his correctness result for the algorithm by Sulzmann and
+  Lu, he proved the correctness of various stages of optimisations: POSIX
+  matching including simplification of regular expressions; bit-coded
+  representation of regular expressions has not yet been done, but
+  should be easy to do in the remaining time
+\end{itemize}  
+
+\noindent
+Part 2 (TLS protocol in F-Star/internship at Microsoft Research in Cambridge)
+
+\begin{itemize}
+\item he added features to the F-Star language in order to verify their
+  TLS parser in F-Star
+  
+\item he created a verified byte-library for F-Star, which provides an
+  API to manipulate byte sequences and indexed arrays 
+
+\item he modified the existing TLS parser in F-Star to use his new byte
+  library for the representation of strings
+
+\item verification of the parser is not yet done, but the hope is
+  he finishes this by the end of his internship (in Sepember)
+\end{itemize}
+
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: