| 1 | % bandali-cv.tex --- bandali's curriculum vitae -*-latex-*- |
| 2 | |
| 3 | % Copyright (C) 2016-2020 Amin Bandali <bandali@uwaterloo.ca> |
| 4 | |
| 5 | % This CV is free software: you can redistribute it and/or modify |
| 6 | % it under the terms of the GNU General Public License as published by |
| 7 | % the Free Software Foundation, either version 3 of the License, or |
| 8 | % (at your option) any later version. |
| 9 | |
| 10 | % This CV is distributed in the hope that it will be useful, |
| 11 | % but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 12 | % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| 13 | % GNU General Public License for more details. |
| 14 | |
| 15 | % You should have received a copy of the GNU General Public License |
| 16 | % along with this CV. If not, see <https://www.gnu.org/licenses/>. |
| 17 | |
| 18 | % With inspirations from Jason Blevins's CV <https://jblevins.org/cv>. |
| 19 | |
| 20 | |
| 21 | \documentclass[letterpaper]{article} |
| 22 | |
| 23 | \def\name{Amin Bandali} |
| 24 | \def\site{bndl.org} |
| 25 | \def\siteurl{https://\site} |
| 26 | \def\pubs#1{\siteurl/publications\##1} |
| 27 | \def\mail{bandali@uwaterloo.ca} |
| 28 | \def\nday{https://cs.uwaterloo.ca/~nday/} |
| 29 | |
| 30 | %% package imports |
| 31 | \usepackage{geometry} % setting page geometry |
| 32 | \usepackage{enumitem} % enumerate with [resume] option |
| 33 | \usepackage{fontspec} % needs LuaTeX |
| 34 | \usepackage{sectsty} % custom section fonts |
| 35 | \usepackage{hyperref} % for PDF metadata |
| 36 | \usepackage{fancyhdr} % fine control of headers/footers |
| 37 | \usepackage{lastpage} % as the name says :-) |
| 38 | |
| 39 | %% PDF metadata |
| 40 | \hypersetup{ |
| 41 | pdfstartview={FitH}, % (H for horizontal) |
| 42 | pdftitle={\name: Curriculum Vitae}, |
| 43 | pdfauthor={\name}, |
| 44 | pdfsubject={Curriculum Vitae}, |
| 45 | pdfkeywords={formal methods, formal logic, model checking, |
| 46 | verification, type systems, interactive theorem provers, |
| 47 | functional programming, lean prover, haskell}, |
| 48 | pdfpagemode=UseNone, |
| 49 | pdfcreator={GNU Emacs 28.0.50}, |
| 50 | pdflang={English}, |
| 51 | pdfnewwindow=true, |
| 52 | colorlinks=true, |
| 53 | urlcolor=black |
| 54 | } |
| 55 | |
| 56 | %% page geometry |
| 57 | \geometry{ |
| 58 | %% bottom=1.25in, |
| 59 | body={6.5in, 9.0in}, |
| 60 | left=1.0in, |
| 61 | top=1.0in |
| 62 | } |
| 63 | |
| 64 | %% footer setup |
| 65 | \pagestyle{fancy} |
| 66 | \fancyhf{} % clear existing header/footer |
| 67 | \renewcommand\headrulewidth{0pt} |
| 68 | \cfoot{% |
| 69 | \textsc{\addfontfeature{Letters=UppercaseSmallCaps,LetterSpace=6.0}% |
| 70 | Bandali CV \textemdash{} page \thepage{} of \pageref*{LastPage}}} |
| 71 | |
| 72 | %% body text font |
| 73 | \usepackage[lining, tabular]{ebgaramond} |
| 74 | \setmonofont[Scale=0.87]{inconsolata} |
| 75 | \setsansfont[Scale=0.95]{Jost} |
| 76 | |
| 77 | %% title font |
| 78 | \newfontfamily\titleface{Linux Libertine O} |
| 79 | \newcommand{\titlefont}[1]{{\titleface\large\addfontfeature{LetterSpace=6.0}\MakeUppercase{#1}}} |
| 80 | |
| 81 | %% section heading font |
| 82 | \newfontfamily\sectionface{Linux Libertine O} |
| 83 | \sectionfont{\sectionface\mdseries\normalsize\uppercase} |
| 84 | \subsectionfont{\sectionface\mdseries\normalsize\itshape} |
| 85 | |
| 86 | %% don't indent paragraphs |
| 87 | \setlength\parindent{0em} |
| 88 | |
| 89 | %% omit itemize bullets, set more compact spacing |
| 90 | \renewenvironment{itemize}{ |
| 91 | \begin{list}{}{ |
| 92 | \setlength{\leftmargin}{1.5em} |
| 93 | \setlength{\itemsep}{0.25em} |
| 94 | \setlength{\parskip}{0em} |
| 95 | \setlength{\parsep}{0.25em} |
| 96 | } |
| 97 | }{ |
| 98 | \end{list} |
| 99 | } |
| 100 | \setlist[enumerate]{itemsep=0.25em} |
| 101 | |
| 102 | %% month and year only |
| 103 | \renewcommand{\today}{\ifcase \month \or January\or February\or March% |
| 104 | \or April\or May \or June\or July\or August\or September\or October% |
| 105 | \or November\or December\fi% |
| 106 | \space \number \year} |
| 107 | |
| 108 | %% various command definitions |
| 109 | \newcommand{\tla}{TLA${}^+$} |
| 110 | |
| 111 | |
| 112 | \begin{document} |
| 113 | |
| 114 | \titlefont{\name} |
| 115 | |
| 116 | \bigskip |
| 117 | \today |
| 118 | |
| 119 | \medskip |
| 120 | \href{\siteurl}{\addfontfeature{LetterSpace=2.0}\site}\\ |
| 121 | \href{mailto:\mail}{\mail}\\ |
| 122 | |
| 123 | \section*{Education} |
| 124 | |
| 125 | \begin{itemize} |
| 126 | \item Master of Mathematics in Computer Science, University of |
| 127 | Waterloo, 2020. |
| 128 | % completed July 14, 2020 |
| 129 | \begin{itemize} |
| 130 | \item Thesis: A Comprehensive Study of Declarative Modelling |
| 131 | Languages. |
| 132 | \item Supervisor: \href{\nday}{Dr. Nancy~A. Day}. \ GPA: 3.7/4.0. |
| 133 | \end{itemize} |
| 134 | \item Bachelor of Science with Honours in Computer Science, York |
| 135 | University, 2017. |
| 136 | % completed December 2017 |
| 137 | \end{itemize} |
| 138 | |
| 139 | \section*{Research Interests} |
| 140 | |
| 141 | \begin{itemize} |
| 142 | \item Formal Logic, Model Checking, Theorem Proving, Verification |
| 143 | \end{itemize} |
| 144 | |
| 145 | \section*{Publications \& Presentations} |
| 146 | |
| 147 | \begin{itemize} |
| 148 | \item \href{\siteurl/mmath}{\textsf{A Comprehensive Study of |
| 149 | Declarative Modelling Languages}}\\ \href{\siteurl}{Amin Bandali}, |
| 150 | \textit{Master's thesis}, University of Waterloo, 2020. |
| 151 | \item \href{\pubs{DBLP:conf/re/AbbassiBDS18}}{\textsf{A Comparison |
| 152 | of the Declarative Modelling Languages B, Dash, and \tla}}\\ Ali |
| 153 | Abbassi, \href{\siteurl}{Amin Bandali}, \href{\nday}{Nancy~A. Day}, |
| 154 | and Jose Serna. \textit{Proc. MoDRE@RE 2018}. |
| 155 | \item \textsf{The magic of specifications and type systems} {\small{} |
| 156 | (\href{\pubs{bandali-magic-lassonde-2017}}{poster}, |
| 157 | \href{\pubs{bandali-magic-cucsc-2017}}{slides})}\\ \href{\siteurl}{Amin |
| 158 | Bandali}, \href{https://github.com/cipher1024}{Simon Hudon}, and |
| 159 | \href{https://www.eecs.yorku.ca/~jonathan/}{Jonathan S. Ostroff}. |
| 160 | Presented at the Canadian Undergraduate Computer Science Conference |
| 161 | 2017, and at the 2017 Lassonde Undergraduate Summer Student Research |
| 162 | Conference. |
| 163 | \end{itemize} |
| 164 | |
| 165 | \section*{Work Experience} |
| 166 | |
| 167 | \subsection*{Free Software Foundation (FSF)} |
| 168 | \begin{itemize} |
| 169 | \item |
| 170 | \begin{description}[font=\mdseries] |
| 171 | \item[spring 2020] Tech team intern |
| 172 | |
| 173 | Working in a sysadmin role on a variety of tasks including |
| 174 | installation of the Sourcehut free software forge on the FSF |
| 175 | infrastructure for evaluation for the FSF forge project, as well |
| 176 | as a series of enhancements for |
| 177 | \href{https://www.gnu.org}{www.gnu.org}. |
| 178 | \end{description} |
| 179 | \end{itemize} |
| 180 | |
| 181 | \subsection*{Cheriton School of Computer Science, University of Waterloo} |
| 182 | \begin{itemize} |
| 183 | \item TA: Teaching Assistant, marking exams and assignments. IA: |
| 184 | Instructional Apprentice, holding tutorials and marking |
| 185 | \item |
| 186 | \begin{description}[font=\mdseries] |
| 187 | \item[SE 465 (Software Testing and Quality Assurance)] TA in winter |
| 188 | 2020. |
| 189 | \item[SE 212 (Logic and Computation)] IA in fall 2019, TA in fall |
| 190 | 2018. |
| 191 | \item[SE 463 (Software Requirements Specification and Analysis)] TA |
| 192 | in spring 2019 and 2018. |
| 193 | \item[CS 136 (Elementary Algorithm Design and Data Abstraction)] TA |
| 194 | in winter 2018. |
| 195 | \end{description} |
| 196 | \end{itemize} |
| 197 | |
| 198 | \subsection*{Dept. of Electrical Engineering \& Computer Science, York University} |
| 199 | \begin{itemize} |
| 200 | \item |
| 201 | \begin{description}[font=\mdseries] |
| 202 | \item[EECS 1012 (Net-Centric Introduction to Computing)] TA in fall |
| 203 | 2017. |
| 204 | \end{description} |
| 205 | \end{itemize} |
| 206 | |
| 207 | \subsection*{Software Engineering Lab, York University} |
| 208 | \begin{itemize} |
| 209 | \item |
| 210 | \begin{description}[font=\mdseries] |
| 211 | \item[summer 2017] Research Assistant |
| 212 | |
| 213 | Worked on an implementation of |
| 214 | \href{https://bertrandmeyer.com/2014/12/07/lampsort/}{\textsf{Lampsort}} |
| 215 | in Eiffel. Extended the |
| 216 | \href{https://svn.eecs.yorku.ca/repos/sel-open/mathmodels/}{\textsf{mathmodels}} |
| 217 | library, implementing a \textsc{rational} class for working with |
| 218 | arbitrarily large rational numbers. |
| 219 | \item[summer 2016] Research Student |
| 220 | |
| 221 | Worked on \textit{Literate Unit-B}, the verifier for Unit-B, a new |
| 222 | formal method focused on formal verification of reactive, |
| 223 | concurrent and distributed systems. From the Literate Unit-B |
| 224 | codebase (written in Haskell), decoupled the logic module and used |
| 225 | it to build \textit{Unit-B Web}, a web interface using Literate |
| 226 | Unit-B to do predicate calculus proofs. Unit-B Web, also written |
| 227 | in Haskell, supports the \LaTeX{} syntax of the Unit-B logic, |
| 228 | renders user input on the page, and calls the sequent prover of |
| 229 | the logic module, which uses the Z3 SMT solver to check the |
| 230 | validity of user input. |
| 231 | |
| 232 | Separated Literate Unit-B's type checker from its parser in a |
| 233 | large refactoring, allowing easier substitution of other type |
| 234 | checking algorithms, and in preparation for implementing |
| 235 | subtyping. |
| 236 | \end{description} |
| 237 | \end{itemize} |
| 238 | |
| 239 | \subsection*{Lotek Wireless Inc.} |
| 240 | \begin{itemize} |
| 241 | \item |
| 242 | \begin{description}[font=\mdseries] |
| 243 | \item[summer 2016] Software Developer |
| 244 | |
| 245 | Designed and developed an Employee Portal web application in C\# |
| 246 | and the MVC framework, used by employees for accessing various |
| 247 | data catalogs and archives. |
| 248 | \item[summer 2015] Software Developer |
| 249 | |
| 250 | Designed and implemented various applications in C\# and C for |
| 251 | analyzing and testing a satellite pass prediction algorithm for |
| 252 | predicting the pass windows of Argos satellites, for scheduling |
| 253 | send times of data collected by the company's wildlife tracking |
| 254 | products. |
| 255 | \end{description} |
| 256 | \end{itemize} |
| 257 | |
| 258 | \subsection*{Athlete Builder} |
| 259 | \begin{itemize} |
| 260 | \item |
| 261 | \begin{description}[font=\mdseries] |
| 262 | \item[2013--2014] Software Developer |
| 263 | |
| 264 | Developed the Backend of Athlete Builder platform in C\# and MVC. |
| 265 | |
| 266 | Key role in development of the platform core. |
| 267 | |
| 268 | Developed the alpha version of Athlete Builder Android application |
| 269 | in Java. |
| 270 | \end{description} |
| 271 | \end{itemize} |
| 272 | |
| 273 | \section*{Community Service} |
| 274 | |
| 275 | \subsection*{EmacsConf Conference} |
| 276 | |
| 277 | \begin{itemize} |
| 278 | \item |
| 279 | \begin{description}[font=\mdseries] |
| 280 | \item[\href{https://emacsconf.org}{2019--present}] Chief organizer |
| 281 | and maintainer of conference infrastructure, including the |
| 282 | streaming servers. |
| 283 | \item[\href{https://emacsconf.org/2015/}{2015}\phantom{--present}] |
| 284 | One of the organizers and in charge of setting up and maintaining |
| 285 | vital pieces of infrastructure. |
| 286 | \end{description} |
| 287 | \end{itemize} |
| 288 | |
| 289 | \subsection*{Computer Science Club (CSC) of the University of Waterloo} |
| 290 | |
| 291 | \begin{itemize} |
| 292 | \item Served as the CSC System Administrator in Winter and Spring |
| 293 | 2020. Present member of the CSC Systems Committee, overseeing and |
| 294 | maintaining a large fleet of GNU/Linux servers for CSC members, as |
| 295 | well as running the CSC mirror for free software projects. |
| 296 | |
| 297 | Notable projects include |
| 298 | \href{https://mailman.csclub.uwaterloo.ca/pipermail/csc-general/2020-July/000837.html}{launching |
| 299 | the CSC web IRC client} as part of an effort in bringing modern |
| 300 | user freedom- and privacy-respecting communication tools to club |
| 301 | members. |
| 302 | \end{itemize} |
| 303 | |
| 304 | \subsection*{Free/Libre Software Contributions} |
| 305 | |
| 306 | \begin{itemize} |
| 307 | \item Co-maintainer of |
| 308 | \href{https://www.gnu.org/software/gnuzilla/gnuzilla.html}{GNUzilla |
| 309 | and IceCat}, the GNU version of the Mozilla suite and the Firefox |
| 310 | browser respectively. |
| 311 | \item Maintainer of |
| 312 | \href{https://www.gnu.org/software/emacs/erc.html}{ERC}, the |
| 313 | powerful, modular, and extensible IRC client distributed with |
| 314 | GNU~Emacs. |
| 315 | \item Committer and regular contributor to |
| 316 | \href{https://www.gnu.org/software/emacs/emacs.html}{GNU~Emacs} and |
| 317 | \href{https://guix.gnu.org}{GNU~Guix}. |
| 318 | \item |
| 319 | \href{https://www.gnu.org/people/webmeisters.html#bandali}{GNU~webmaster} |
| 320 | and |
| 321 | \href{https://savannah.gnu.org/maintenance/SavannahHacker/}{GNU~Savannah |
| 322 | hacker}. |
| 323 | \end{itemize} |
| 324 | |
| 325 | \subsection*{Volunteer Work} |
| 326 | |
| 327 | \begin{itemize} |
| 328 | \item |
| 329 | \begin{description}[font=\mdseries] |
| 330 | \item[spring 2013] Application Developer for VONICAL Inc. |
| 331 | |
| 332 | Worked on development of the Employment Accessibility Resource |
| 333 | Network (EARN) portal using the Anahita social networking |
| 334 | platform, written in PHP and running on GNU/Linux. |
| 335 | \end{description} |
| 336 | \item |
| 337 | \begin{description}[font=\mdseries] |
| 338 | \item[winter 2013] Mobile \& Web Developer for Hire Works Inc. |
| 339 | |
| 340 | Worked on a variety of web and mobile development projects for |
| 341 | Hire Works. |
| 342 | \end{description} |
| 343 | \item |
| 344 | \begin{description}[font=\mdseries] |
| 345 | \item[summer 2012] Web Developer for St. Brigid's Summer Camp |
| 346 | |
| 347 | Redesigned and revamped the codebase for the photo gallery section |
| 348 | of the camp's website in PHP and JavaScript. |
| 349 | \end{description} |
| 350 | \end{itemize} |
| 351 | |
| 352 | %% TODO? \section*{Recent Projects} |
| 353 | |
| 354 | %% \section*{Achievements} |
| 355 | |
| 356 | %% \begin{itemize} |
| 357 | %% \item Was among the top 1\% incoming students in Carleton University's |
| 358 | %% undergraduate Computer Science program, and a top student in the |
| 359 | %% faculty of science. |
| 360 | %% \item Highest standing in Computer Science in grade 11 (92\%) and |
| 361 | %% grade 12 (100\%) at High school at Glebe~Collegiate~Institute. |
| 362 | %% \item Ranked in the top 25\% in the Canadian Senior Mathematics |
| 363 | %% Contest held by University of Waterloo, in 2013 (grade 11). |
| 364 | %% \item Graduated from high school with an average of 95\%; and |
| 365 | %% designated as an Ontario Scholar. |
| 366 | %% \end{itemize} |
| 367 | |
| 368 | \section*{Miscellaneous} |
| 369 | |
| 370 | \begin{itemize} |
| 371 | \item \textit{Programming Languages:} Haskell, Python, C, Emacs Lisp, |
| 372 | Guile Scheme, Eiffel, Rust, C\#, Java, JavaScript. |
| 373 | \item \textit{Tools:} GNU Emacs, Git, Alloy, \tla, ProB, \LaTeX, |
| 374 | continuous integration systems. |
| 375 | \item \textit{Platforms:} GNU/Linux distributions, including Trisquel, |
| 376 | GNU Guix, Debian. |
| 377 | \item \textit{Languages:} Persian (mother tongue), English (fluent), French |
| 378 | (beginner). |
| 379 | \end{itemize} |
| 380 | |
| 381 | \end{document} |