Commit | Line | Data |
---|---|---|
88457a37 AB |
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} |