1 \documentclass[11pt]{article}

     2 \usepackage{times}

     3 \usepackage{amsmath}

     4 \usepackage{amssymb}

     5 

     6 \begin{document}

     7 

     8 \noindent

     9 {\LARGE\bf Fahad's results for thesis}\bigskip

    10 

    11 \noindent

    12 Part 1 (regular expressions)

    13 

    14 \begin{itemize}

    15 \item he corrected the paper by Sulzmann and Lu by giving a new definition

    16   for POSIX matching---his proof is completely different than the one

    17   by Sulzmann and Lu and formalised in Isabelle

    18   

    19 \item he extended the results by Sulzmann and Lu to all regular

    20   expression constructors, excluding back references; to deal with

    21   backreferences is probably too difficult for the remaining time

    22 

    23 \item he formalised in Isabelle the definition of POSIX matching by Okui and

    24   Suzuki and showed that it is equivalent to his definition (his

    25   definition is declarative, whereas the one by Okui \& Suzuki is by a

    26   position caluculus---so both definitions are quite different

    27   technically, but the result is that they define the same `thing')

    28 

    29 \item from his correctness result for the algorithm by Sulzmann and

    30   Lu, he proved the correctness of various stages of optimisations: POSIX

    31   matching including simplification of regular expressions; bit-coded

    32   representation of regular expressions has not yet been done, but

    33   should be easy to do in the remaining time

    34 \end{itemize}  

    35 

    36 \noindent

    37 Part 2 (TLS protocol in F-Star/internship at Microsoft Research in Cambridge)

    38 

    39 \begin{itemize}

    40 \item he added features to the F-Star language in order to verify their

    41   TLS parser in F-Star

    42   

    43 \item he created a verified byte-library for F-Star, which provides an

    44   API to manipulate byte sequences and indexed arrays 

    45 

    46 \item he modified the existing TLS parser in F-Star to use his new byte

    47   library for the representation of strings

    48 

    49 \item verification of the parser is not yet done, but the hope is

    50   he finishes this by the end of his internship (in Sepember)

    51 \end{itemize}

    52 

    53 

    54 \end{document}

    55 

    56 %%% Local Variables:

    57 %%% mode: latex

    58 %%% TeX-master: t

    59 %%% End: