[~bandali/cv] / cv.tex

%% cv.tex
%% Copyright 2016-2019 Amin Bandali <mab@gnu.org>
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% Based on Jason R. Blevins's Curriculum Vitae template,
% Copyright (C) 2004-2016 Jason R. Blevins <jrblevin@sdf.org>
% http://jblevins.org/

\documentclass[12pt,letterpaper]{article}

\usepackage{hyperref}
\usepackage{geometry}
\usepackage{enumitem}
\usepackage{fancyhdr}
\usepackage{lastpage}
% To enable correct spacing
\usepackage{xspace}
\pagestyle{fancy}

% Fonts
\usepackage{graphicx}
\usepackage[cmintegrals,cmbraces]{newtxmath}
\usepackage{ebgaramond-maths}
\usepackage[sf]{libertine}
\usepackage[scale=0.87]{inconsolata}
\usepackage[T1]{fontenc}
\newcommand{\amper}{{\selectfont\itshape\&}}

\newcommand{\tla}{TLA${}^+$}

\def\name{Amin Bandali}

% The following metadata will show up in the PDF properties
\hypersetup{
  colorlinks = true,
  urlcolor = black,
  pdfauthor = {\name},
  pdfkeywords = {Formal Methods, Formal Logic, Model Checking,
    Verification, Type Systems, Proof Systems, Interactive Provers,
    Programming Languages, Functional Programming, Haskell, Rust},
  pdftitle = {\name: Curriculum Vitae},
  pdfsubject = {Curriculum Vitae},
  pdfpagemode = UseNone
}

\geometry{
  body={6.5in, 9.0in},
  left=1.0in,
  top=1.0in
}

\pagestyle{fancy}
\fancyhf{}% to clear existing header/footer
\renewcommand\headrulewidth{0pt}
\cfoot{\vspace*{-.25em}\textsc{bandali cv --- page
    \thepage \xspace of \pageref*{LastPage}}}

% Custom section fonts
\usepackage{sectsty}
\sectionfont{\rmfamily\mdseries\Large}
\subsectionfont{\rmfamily\mdseries\itshape\large}

% Other possible font commands include:
% \ttfamily for teletype,
% \sffamily for sans serif,
% \bfseries for bold,
% \scshape for small caps,
% \normalsize, \large, \Large, \LARGE sizes.

% Don't indent paragraphs.
\setlength\parindent{0em}

% Make lists without bullets and compact spacing
\renewenvironment{itemize}{
  \begin{list}{}{
    \setlength{\leftmargin}{1.5em}
    \setlength{\itemsep}{0.25em}
    \setlength{\parskip}{0pt}
    \setlength{\parsep}{0.25em}
  }
}{
  \end{list}
}
\setlist[enumerate]{itemsep=0.25em}

\begin{document}

\vspace*{-3em}

% Place name at left
{\huge \name}

% Alternatively, print name centered and bold:
%\centerline{\huge \bf \name}

\medskip

\begin{minipage}[t]{0.495\textwidth}
  site: \href{https://bandali.eu.org}{bandali.eu.org} \\
  email: \href{mailto:bandali@uwaterloo.ca}{bandali@uwaterloo.ca} \\
  phone: available upon request
\end{minipage}

\vspace*{1em}

\section*{Education}

\begin{itemize}
  \setlength\itemsep{.75em}

\item {\large Master of Mathematics (Computer Science)}\, |\, {\small 2018--present}

  \textit{University of Waterloo}, Canada

  \begin{itemize}
  \item Supervised by Dr. Nancy Day | GPA: 3.7/4.0 | Expected
    completion: Winter 2020
  \item Research focusing on formal logic, model checking, and verification.
  \end{itemize}

\item {\large B.Sc. Honours Computer Science}\, |\, {\small 2013--2017}

  \textit{York University}, Toronto, Canada

  \begin{itemize}
  \item GPA: 7.84/9.0
  \item Relevant courses: System Specification \amper\
    Refinement, Software Requirements Eng., Software Design, Operating
    Systems, Computational Complexity, Design \amper\ Analysis of Algorithms.
  \item Finished first year (2013-14) at \textit{Carleton University} with a GPA
    of 11.0/12.0, then transferred to \textit{York University} in Fall 2014.
  \end{itemize}

\end{itemize}

\section*{Publications}

\begin{itemize}
\item {\large MoDRE 2018}

  \begin{itemize}
  \item \textsf{A Comparison of the Declarative Modelling Languages B,
    Dash, and \tla} \textsf{\footnotesize
    (\href{https://bandali.eu.org/papers/modre2018-declarative.pdf}{pdf},
    \href{https://bandali.eu.org/papers/modre2018-declarative.bib}{bib})}

    Ali Abbassi, Amin Bandali, Nancy A. Day, and Jose Serna\\
    \textit{2018 IEEE 8th International Model-Driven Requirements
      Engineering Workshop (MoDRE)}
  \end{itemize}

\end{itemize}

\section*{Work \amper\ Research Experience}

\begin{itemize}

\item {\large Cheriton School of Computer Science, } University of Waterloo\, |\, {\small 2018--present}

  \textit{Instructional Apprentice (IA), Teaching Assistant (TA)}

  \begin{itemize}
  \item \textsf{\small SE 212} (Logic and Computation): IA in Fall
    2019, TA in Fall 2018
  \item \textsf{\small SE 463} (Software Requirements Specification
    and Analysis): TA in Summer 2019 and 2018
  \item \textsf{\small CS 136} (Elementary Algorithm Design and Data
    Abstraction): TA in Winter 2018
  \end{itemize}

\item {\large EECS Department, } York University\, |\, {\small fall 2017}

  \textit{Teaching Assistant}

  \begin{itemize}
  \item I was a TA for \textsf{\small EECS 1012}, Net-Centric
    Introduction to Computing, taught by Dr. Brown.
  \end{itemize}

  \pagebreak

\item {\large Software Engineering Lab, } York University\, |\, {\small summer
  2017}

  \textit{Research Assistant}

  \begin{itemize}
  \item I worked on an implementation of
    \href{https://bertrandmeyer.com/2014/12/07/lampsort/}{\textit{Lampsort}} in
    Eiffel. I also extended the
    \href{https://svn.eecs.yorku.ca/repos/sel-open/mathmodels/}{\texttt{mathmodels}}
    library, implementing a \textsc{rational} class for working with arbitrarily
    large rational numbers.
  \end{itemize}

\item {\large Software Engineering Lab, } York University\, |\, {\small summer
    2016}

  \textit{Research Student}

  \begin{itemize}
  \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.  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 \textsc{z3 smt} solver to check the validity of user input.

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

\section*{Conference Presentations}

\begin{itemize}
\item {\large CUCSC 2017}

  \begin{itemize}
  \item \textsf{The Magic of Specifications and Type Systems}
    (\href{https://bandali.eu.org/talks/cucsc-2017-slides.pdf}{slides}),
    at Canadian Undergraduate Computer Science Conference, University
    of Toronto, Canada, Jun 15--17 2017.
  \end{itemize}

\item {\large Lassonde USSR Conference 2017}

  \begin{itemize}
  \item \textsf{The Magic of Specifications and Type Systems}
    (\href{https://bandali.eu.org/talks/eecs4080-poster.pdf}{poster}),
    at Lassonde Undergraduate Summer Student Research Conference, York
    University, Toronto, Canada, August 15, 2017.
  \end{itemize}

\end{itemize}

\section*{Professional Experience}
\begin{itemize}
\item {\large Lotek Wireless Inc., } Newmarket, Canada\, |\, {\small
  summer 2015 \amper\ 2016}

  \textit{Software Developer}

  \begin{itemize}
  \item Designed and implemented various applications in C\# and C to test and
    analyze a satellite pass prediction algorithm for predicting the pass
    windows of Argos satellites, for scheduling send times of data collected by
    company's wildlife tracking products.

  \item Designed and developed an Employee Portal web application in C\# and the
    MVC framework, used by employees for accessing various data catalogs and
    archives.
  \end{itemize}
  \vspace{.25em}

\pagebreak  % TODO: remove if necessary

\item {\large Athlete Builder, } Ottawa, Canada\, |\, {\small 2013--2014}

  \textit{Software Developer}

  \begin{itemize}
  \item Developed the Backend of Athlete Builder platform in C\# and MVC.
  \item Was a key role in development of the platform core.
  \item Developed the alpha version of Athlete Builder Android app in Java.
  \end{itemize}
\end{itemize}

\section*{Volunteer Activities}

\begin{itemize}

\item {\large EmacsConf 2019, } \href{https://emacsconf.org/2019}{\texttt{emacsconf.org/2019}}\, |\,
  {\small fall 2019}

  \textit{Organizer}

  \begin{itemize}
  \item I was the chief organizer for EmacsConf 2019, and in charge of
    maintaining and overseeing the EmacsConf infrastructure, including
    our streaming servers.
  \end{itemize}
  \vspace{.25em}

\item {\large Computer Science Club, } University of Waterloo,
  Canada\, |\, {\small summer 2019--present}

  \textit{Systems Committee}

  \begin{itemize}
  \item I'm a member of the CSC syscom at the University of Waterloo,
    operating and maintaining the club's fleet of GNU/Linux servers.
  \end{itemize}
  \vspace{.25em}

\item {\large EmacsConf 2015, } \href{https://emacsconf.org/2015}{\texttt{emacsconf.org/2015}}\, |\,
  {\small summer 2015}

  \textit{Organizer}

  \begin{itemize}
  \item I was one of the organizers and in charge of setting up and
    maintaining several vital pieces of the EmacsConf infrastructure.
  \end{itemize}
  \vspace{.25em}

\item {\large VONICAL Inc., } Ottawa, Canada\, |\, {\small spring 2013}

  \textit{Application Developer}

  \begin{itemize}
  \item As a volunteer, worked on development of EARN (Employment Accessibility
    Resource Network) portal using the Anahita social networking platform, in
    PHP under Linux.
  \end{itemize}
  \vspace{.25em}

\item {\large Hire Works Inc., } Ottawa, Canada\, |\, {\small winter 2013}

  \textit{Mobile \& Web Developer}

  \begin{itemize}
  \item As a volunteer, I worked on a variety of web and mobile projects for
    Hire Works, Inc.
  \end{itemize}
  \vspace{.25em}

\item {\large St. Brigid's Summer Camp, } Ottawa, Canada\, |\, {\small summer
    2012}

  \textit{Web Developer}

  \begin{itemize}
  \item As a volunteer, I re-designed and coded (from scratch) an updated and
    revamped version of the photo gallery section of St. Brigid Summer Camp's
    website in PHP and JavaScript. A refactored version of my code is deployed
    and being used.
  \end{itemize}
  % \vspace{.25em}

\end{itemize}


\section*{Recent Projects}

\begin{itemize}
\item \textit{george-mode:} Emacs major mode for editing George
  files.\\ Source code available at
  \href{https://git.sr.ht/~bandali/george-mode}{\texttt{https://git.sr.ht/\textasciitilde{}bandali/george-mode}}
\item \textit{alloy-catalyst:} Framework for performance analysis of
  Alloy models.\\ Source code available at
  \href{https://git.uwaterloo.ca/bandali/alloy-catalyst}{\texttt{https://git.uwaterloo.ca/bandali/alloy-catalyst}}
\item \textit{Unit-B Web:} The web interface for Unit-B, as mentioned in the
  \textit{Research Experience} section.\\
  Source code available at
  \href{https://github.com/unitb/unitb-web}{\texttt{https://github.com/unitb/unitb-web}}

\item \textit{tex2png-hs:} A tool for easily converting \TeX\ and \LaTeX\ to
  \textsc{png} images. \texttt{tex2png-hs} is a Haskell port of Xyne's
  \texttt{tex2png} tool. It is a wrapper around \texttt{latex} and
  \texttt{dvipng} and provides several options for modifying its behaviour, such
  as cropping the whitespace around the content, specifying the \textsc{dpi}, or
  inputting a full document.\\
  Source code available at
  \href{https://github.com/unitb/tex2png-hs}{\texttt{https://github.com/unitb/tex2png-hs}}

\item For more projects, visit my personal site at
  \href{https://bandali.eu.org}{\texttt{https://bandali.eu.org}}.
\end{itemize}

\section*{Miscellaneous}

\begin{itemize}
\item \textit{Programming Languages:} Haskell, Python, C, Emacs Lisp,
  Guile, Eiffel, Rust, C\#, Java, JavaScript.
\item \textit{Tools:} Emacs, Git, Alloy, \tla, \LaTeX, CI
  systems, Rodin, Liquid Haskell.
\item \textit{Platforms:} GNU/Linux distributions including GNU Guix,
  Trisquel, Parabola, Debian.
\item \textit{Languages:} Persian (mother tongue), English (fluent), French
  (beginner).
\end{itemize}


% \section*{Achievements}

% \begin{itemize}
% \item Was among the top 1\% incoming students in Carleton University's
%   undergraduate Computer Science program, and a top student in the faculty of
%   science.
% \item Highest standing in Computer Science in grade 11 (92\%) and grade 12
%   (100\%) at High school at Glebe~Collegiate~Institute.
% \item Ranked in the top 25\% in the Canadian Senior Mathematics Contest held by
%   University of Waterloo, in 2013 (grade 11).
% \item Graduated from high school with an average of 95\%; and designated as an Ontario Scholar.
% \end{itemize}


% Footer
\bigskip
{\small Last updated: \today}

\end{document}