summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
9bbaaec)
(separating the type checker from the parser)
-%% Copyright 2016 Amin Bandali <amin@aminb.org>
+%% Copyright 2016-2017 Amin Bandali <amin@aminb.org>
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
\textit{Research Student}
\begin{itemize}
\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
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}
\end{itemize}
\end{itemize}