Mention my work on Literate Unit-B's type checker
[~bandali/cv] / cv.tex
CommitLineData
d99d2f71 1%% cv.tex
10664de5 2%% Copyright 2016-2017 Amin Bandali <amin@aminb.org>
8a25c428 3%
d99d2f71
AB
4% This work may be distributed and/or modified under the
5% conditions of the LaTeX Project Public License, either version 1.3
6% of this license or (at your option) any later version.
7% The latest version of this license is in
8% http://www.latex-project.org/lppl.txt
9% and version 1.3 or later is part of all distributions of LaTeX
10% version 2005/12/01 or later.
8a25c428
AB
11%
12% Based on Jason R. Blevins's Curriculum Vitae template,
13% Copyright (C) 2004-2016 Jason R. Blevins <jrblevin@sdf.org>
14% http://jblevins.org/
8a25c428
AB
15
16\documentclass[12pt,letterpaper]{article}
17
18\usepackage{hyperref}
19\usepackage{geometry}
20\usepackage{enumitem}
21
22% Fonts
23\usepackage{graphicx}
24\usepackage{fontspec}
25\setmainfont[Numbers=Lining]{EB Garamond}
26\newfontfamily{\smallcaps}[RawFeature={+c2sc,+scmp}]{EB Garamond}
8a25c428
AB
27\newcommand{\amper}{{\fontspec[Scale=.9]{EB Garamond}\selectfont\itshape\&}}
28
29%% Load Microtype with default settings. This will use the
30%% EB-Garamond protrusion definitions if present.
31\usepackage{microtype}
32
33
34\def\name{Amin Bandali}
35
36% The following metadata will show up in the PDF properties
37\hypersetup{
38 colorlinks = true,
39 urlcolor = black,
40 pdfauthor = {\name},
41 pdfkeywords = {Programming Languages, Haskell, Rust, Formal Methods, Type
42 Systems, Proof Systems, Automated Provers},
43 pdftitle = {\name: Curriculum Vitae},
44 pdfsubject = {Curriculum Vitae},
45 pdfpagemode = UseNone
46}
47
48\geometry{
49 body={6.5in, 9.0in},
50 left=1.0in,
51 top=1.0in
52}
53
54% Customize page headers
55\pagestyle{myheadings}
56\markright{\name}
57\thispagestyle{empty}
58
59% Custom section fonts
60\usepackage{sectsty}
61\sectionfont{\rmfamily\mdseries\Large}
62\subsectionfont{\rmfamily\mdseries\itshape\large}
63
64% Other possible font commands include:
65% \ttfamily for teletype,
66% \sffamily for sans serif,
67% \bfseries for bold,
68% \scshape for small caps,
69% \normalsize, \large, \Large, \LARGE sizes.
70
71% Don't indent paragraphs.
72\setlength\parindent{0em}
73
74% Make lists without bullets and compact spacing
75\renewenvironment{itemize}{
76 \begin{list}{}{
77 \setlength{\leftmargin}{1.5em}
78 \setlength{\itemsep}{0.25em}
79 \setlength{\parskip}{0pt}
80 \setlength{\parsep}{0.25em}
81 }
82}{
83 \end{list}
84}
85\setlist[enumerate]{itemsep=0.25em}
86
87\begin{document}
88
89% Place name at left
90{\huge \name}
91
92% Alternatively, print name centered and bold:
93%\centerline{\huge \bf \name}
94
95\bigskip
96
97\begin{minipage}[t]{0.495\textwidth}
98 Email: \href{mailto:amin9@my.yorku.ca}{amin9@my.yorku.ca} \\
99 Homepage: \href{https://aminb.org}{https://aminb.org} \\
100 Phone: available upon request
101\end{minipage}
102
103\section*{Research Interests}
104
105\begin{itemize}
106\item Functional Programming and functional languages
107\item Formal methods, especially type systems, proof systems, and automated
108 provers
109\item Verification, Haskell, and Rust
110\end{itemize}
111
112\section*{Education}
113
114\begin{itemize}
9bbaaec3 115 \setlength\itemsep{.75em}
8a25c428
AB
116\item {\large B.Sc. Honours Computer Science}\, |\, {\small 2013--present}
117
9bbaaec3 118 \textit{York University}, Toronto, Canada
8a25c428
AB
119
120 \begin{itemize}
c543f989
AB
121 \item GPA: 7.9/9.0
122 \item Expected completion: December 2017
123 \item Relevant courses: System Specification \amper\
8a25c428
AB
124 Refinement, Operating System Design, Computational Complexity, Artificial
125 Intelligence \amper\ Logic Programming, Design \amper\ Analysis of
126 Algorithms.
127 \item Finished first year (2013-14) at \textit{Carleton University} with a GPA
128 of 11.0/12.0 then transferred to \textit{York University} in Fall 2014.
129 \end{itemize}
9bbaaec3
AB
130
131\item {\large High School Diploma}\, |\, {\small 2013}
132
133 \textit{Glebe Collegiate Institute}, Ottawa, Canada
134
135 \hspace{1.3em} Average: 94.3\%
8a25c428
AB
136\end{itemize}
137
138\section*{Research Experience}
139
140\begin{itemize}
141\item {\large Software Engineering Lab, } York University\, |\, {\small summer 2016}
142
143 \textit{Research Student}
144
145 \begin{itemize}
10664de5
AB
146 \item As an undergraduate research student, I worked on \textit{Literate
147 Unit-B}, the verifier for Unit-B, a new formal method focused on formal
148 verification of reactive, concurrent and distributed systems.
8a25c428
AB
149
150 From the Literate Unit-B codebase (written in Haskell), I decoupled the
c543f989 151 logic module and used it to build \textit{Unit-B Web}, a web interface using
8a25c428
AB
152 Literate Unit-B to do predicate calculus proofs. \linebreak Unit-B Web, also
153 written in Haskell, supports the \LaTeX\ syntax of the Unit-B logic, renders
10664de5
AB
154 user input on the page, and calls the sequent prover of the logic module,
155 which uses the Z3 SMT solver to check the validity of user input.
8a25c428 156
10664de5
AB
157 \item Further, I separated Literate Unit-B's type checker from its parser,
158 allowing easier substitution of other type checking algorithms and in
159 preparation for implementing subtyping.
8a25c428
AB
160 \end{itemize}
161 \end{itemize}
162
163\section*{Professional Experience}
164\begin{itemize}
165\item {\large Lotek Wireless Inc., } Newmarket, Canada\, |\, {\small 2015--2016}
166
167 \textit{Software Developer}
168
169 \begin{itemize}
170 \item Designed and implemented various applications in C\# and C to test and
171 analyze a satellite pass prediction algorithm for predicting the pass
172 windows of Argos satellites, for scheduling send times of data collected by
173 company's wildlife tracking products.
174
175 \item Designed and developed an Employee Portal web application in C\# and the
176 MVC framework, used by employees for accessing various data catalogs and
177 archives.
178 \end{itemize}
179 \vspace{.25em}
180
181\item {\large Athlete Builder, } Ottawa, Canada\, |\, {\small 2013--2014}
182
183 \textit{Software Developer}
184
185 \begin{itemize}
186 \item Developed the Backend of Athlete Builder platform in C\# and MVC.
187 \item Was a key role in development of the platform core.
188 \item Developed the alpha version of Athlete Builder Android app in Java.
189 \end{itemize}
190\end{itemize}
191
192\section*{Volunteer Activities}
193
194\begin{itemize}
195
196\item {\large EmacsConf 2015, } \href{http://emacsconf.org}{emacsconf.org}\, |\,
197 {\small summer 2015}
198
199 \textit{Organizer}
200
201 \begin{itemize}
202 \item EmacsConf is a conference about the joy of Emacs and writing Emacs
203 Lisp. I was a key organizer and in charge of setting up and maintaining
204 several vital pieces of the EmacsConf infrastructure.
205 \end{itemize}
206 \vspace{.25em}
207
208\item {\large VONICAL Inc., } Ottawa, Canada\, |\, {\small spring 2013}
209
210 \textit{Application Developer}
211
212 \begin{itemize}
213 \item As a volunteer, worked on development of EARN (Employment Accessibility
214 Resource Network) portal using the Anahita social networking platform, in
215 PHP under Linux.
216 \end{itemize}
217 \vspace{.25em}
218
219\item {\large Hire Works Inc., } Ottawa, Canada\, |\, {\small winter 2013}
220
221 \textit{Mobile \& Web Developer}
222
223 \begin{itemize}
224 \item As a volunteer, I worked on a variety of web and mobile projects for
225 Hire Works, Inc.
226 \end{itemize}
227 \vspace{.25em}
228
229\item {\large St. Brigid's Summer Camp, } Ottawa, Canada\, |\, {\small summer
230 2012}
231
232 \textit{Web Developer}
233
234 \begin{itemize}
235 \item As a volunteer, I re-designed and coded (from scratch) an updated and
236 revamped version of the photo gallery section of St. Brigid Summer Camp's
237 website in PHP and JavaScript. A refactored version of my code is deployed
238 and being used.
239 \end{itemize}
240 % \vspace{.25em}
241
242\end{itemize}
243
244
8b20245a
AB
245\section*{Recent Projects}
246
247\begin{itemize}
248\item \textit{Unit-B Web:} The web interface for Unit-B, as mentioned in the
249 \textit{Research Experience} section.\\
250 Source code available at
251 \href{https://github.com/unitb/unitb-web}{https://github.com/unitb/unitb-web}
252
253\item \textit{tex2png-hs:} A tool for easily converting \TeX\ and \LaTeX\ to PNG
254 images. \verb#tex2png-hs# is a Haskell port of Xyne's \verb#tex2png# tool. It
255 is a wrapper around \verb#latex# and \verb#dvipng# and provides several
256 options for modifying its behaviour, such as cropping the whitespace around
257 the content, specifying the DPI, or inputting a full document.\\
258 Source code available at
259 \href{https://github.com/unitb/tex2png-hs}{https://github.com/unitb/tex2png-hs}
260
261\item For more projects, visit my GitHub profile at
262 \href{https://github.com/aminb}{https://github.com/aminb}.
263\end{itemize}
264
8a25c428
AB
265\section*{Miscellaneous}
266
267\begin{itemize}
f18bfd90
AB
268\item \textit{Programming Languages:} Haskell, Rust, Python, C, Emacs Lisp,
269 \LaTeX, C\#, Java, JavaScript.
8a25c428
AB
270\item \textit{Platforms:} Arch Linux, Ubuntu and other distros, Android, macOS,
271 Windows.
f18bfd90 272\item \textit{Tools:} Emacs, Git, Zsh, CI Systems (e.g. Travis CI),
8a25c428 273 Rodin, SQL DBs.
07f3d0ee
AB
274\item \textit{Languages:} Persian (mother tongue), English (fluent), French
275 (beginner).
8a25c428
AB
276\end{itemize}
277
278
279% Footer
280\bigskip
281{\small Last updated: \today}
282
283\end{document}