From: Amin Bandali Date: Tue, 2 May 2017 02:33:21 +0000 (-0400) Subject: Mention my work on Literate Unit-B's type checker X-Git-Url: https://git.shemshak.org/~bandali/cv/commitdiff_plain/10664de5948c0a04d360967ad2df8dfc9600d520?hp=9bbaaec31cabc581fe5cd0947d189c53280c026c Mention my work on Literate Unit-B's type checker (separating the type checker from the parser) --- diff --git a/cv.tex b/cv.tex index 78cdfb9..e48fc28 100644 --- a/cv.tex +++ b/cv.tex @@ -1,5 +1,5 @@ %% cv.tex -%% Copyright 2016 Amin Bandali +%% Copyright 2016-2017 Amin Bandali % % This work may be distributed and/or modified under the % conditions of the LaTeX Project Public License, either version 1.3 @@ -143,21 +143,20 @@ \textit{Research Student} \begin{itemize} - \item Semester project: As an undergraduate research student, I - worked on \textit{Literate Unit-B}, the verifier for Unit-B, a new - formal method focused on formal verification of reactive, concurrent - and distributed systems. + \item As an undergraduate research student, I worked on \textit{Literate + Unit-B}, the verifier for Unit-B, a new formal method focused on formal + verification of reactive, concurrent and distributed systems. From the Literate Unit-B codebase (written in Haskell), I decoupled the logic module and used it to build \textit{Unit-B Web}, a web interface using Literate Unit-B to do predicate calculus proofs. \linebreak Unit-B Web, also written in Haskell, supports the \LaTeX\ syntax of the Unit-B logic, renders - user input on the page, and calls the sequent prover of the logic - module, which uses the Z3 SMT solver to check the validity of user - input. + user input on the page, and calls the sequent prover of the logic module, + which uses the Z3 SMT solver to check the validity of user input. - \item Volunteer work: I'm currently working on implementing subtyping for - Literate Unit-B. + \item Further, I separated Literate Unit-B's type checker from its parser, + allowing easier substitution of other type checking algorithms and in + preparation for implementing subtyping. \end{itemize} \end{itemize}