\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: