-<!doctype html>
-<html lang="en">
-<head>
-<meta charset="utf-8" />
-<meta name="author" content="bandali" />
-<meta name="viewport" content="width=device-width, initial-scale=1" />
-<title>curriculum vitae — bandali</title>
-<link rel="canonical" href="https://bndl.org/cv.html" />
-<link rel="alternate" href="bandali-cv.txt" title="plain text" type="text/plain" />
-<link rel="alternate" href="https://p.bndl.org/bandali-cv.pdf" title="pdf" type="application/pdf" />
-<style>
-body {
- line-height: 1.6;
- max-width: 37.5em;
- margin: 0 auto;
- padding: 0 1em;
-}
-.tex {
- font-family: "Tex Gyre Termes", serif;
- text-transform: uppercase;
-}
-.tex span {
- font-size: 0.75em;
- margin-left: -0.05em;
- margin-right: -0.20em;
-}
-.tex sub {
- font-size: 1em;
- margin-left: -0.1667em;
- margin-right: -0.125em;
- vertical-align: -0.5ex;
-}
-.tex sup {
- font-size: 0.85em;
- margin-left: -0.36em;
- margin-right: -0.15em;
- vertical-align: 0.15em;
-}
-.box {
- background: #f8f8f8;
- border: 1px solid #e6e6e6;
- border-radius: 4px;
- font-size: 0.95em;
- padding: 0.6em 0.9em;
-}
-#link-grid {
- display: grid;
- grid: none / auto 1fr;
- gap: 0.2em 1em;
-}
-#link-grid dd { margin-left: 0; }
-@media (prefers-color-scheme: dark) {
- body { background: #1c1c1c; color: white; }
- a:link { color: #acdeff; }
- a:visited { color: #f8f; }
- a:active { color: #e00; }
- .box { background: #1b1d1e; border-color: #373c34; }
-}
-</style>
-</head>
-<body>
-<h1><a href=".">bandali</a>'s curriculum vitae</h1>
-
-<p class="box">also available in plain text
-as <a href="bandali-cv.txt">bandali-cv.txt</a></p>
-
-<dl id="link-grid">
-<dt>Site</dt>
-<dd><a href="https://bndl.org">bndl.org</a></dd>
-<dt>Email</dt>
-<dd>bandali@gnu.org</dd>
-<dt>Phone</dt>
-<dd>available upon request via email</dd>
-</dl>
-
-<h2>Summary of Qualifications</h2>
-
-<ul>
-<li>Experience in building software for diverse areas and platforms in
-various programming languages such as C, Python, and Haskell.</li>
-<li>Passionate about applying scientific and engineering methods while
-designing and building software systems.</li>
-<li>Using formal specification techniques to find specification-level
-bugs early in the design stage rather than implementation.</li>
-<li>GNU/Linux system administration on both the client and the server
-side.</li>
-<li>Problem-solving and communication skills, honed through research
-and teaching roles held in graduate school, as well as holding
-tutorials discussing complex concepts with fellow students and peers
-throughout undergraduate studies and high school.</li>
-<li>Organizational and teamwork skills, strengthened thanks to
-community service in form of volunteer activities including organizing
-the EmacsConf conference and volunteer work for charities such as the
-Free Software Foundation and St. Brigid's Summer Camp.</li>
-</ul>
-
-<h2>Education</h2>
-
-<dl>
-<dt>Master of Mathematics in Computer Science, University of Waterloo,
-2020</dt>
-<dd>Research focus: formal logic, model checking, verification</dd>
-<dd>Thesis: <a href="#mmath">A Comprehensive Study of Declarative
-Modelling Languages</a></dd>
-<dd>Supervisor: <a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy
-A. Day</a></dd>
-<dd>GPA: 3.7/4.0</dd>
-
-<dt>Bachelor of Science with Honours in Computer Science, York
-University, 2017</dt>
-<dd>Favourite courses: System Specification & Refinement, Software
-Requirements Engineering, Software Design, Operating Systems,
-Computational Complexity, Design & Analysis of Algorithms</dd>
-<dd>GPA: 7.84/9.0</dd>
-</dl>
-
-<h2 id="research">Research Interests</h2>
-
-formal logic, model checking, theorem proving, verification
-
-<h2 id="publications">Publications & Presentations</h2>
-
-<p>The complete bibliography of my publications is available as
-a <a href="bandali.bib">bandali.bib</a>
-<span class="tex">B<span>ib</span>T<sub>e</sub>X</span> bibliography
-file.</p>
-
-<h3>Papers</h3>
-
-<dl>
-<dt>A Comparison of the Declarative Modelling Languages B, DASH, and
-TLA<sup>+</sup>
-<small>
-[ <a href="https://p.bndl.org/modre2018-declarative.pdf">pdf</a>
-| <a href="https://cs.uwaterloo.ca/~nday/artifacts/2018-modre/">models</a>
-]
-</small>
-</dt>
-<dd>
-Ali Abbassi, <a href="https://bndl.org">Amin Bandali</a>,
-<a href="https://cs.uwaterloo.ca/~nday/">Nancy A. Day</a>, Jose Serna<br />
-<em>8th IEEE International Model-Driven Requirements Engineering Workshop, MoDRE@RE 2018</em><br />
-Copyright © 2018 IEEE. All Rights Reserved. Sadly.
-</dd>
-</dl>
-
-<h3>Theses</h3>
-
-<dl>
-<dt id="mmath">A Comprehensive Study of Declarative Modelling
-Languages
-<small>
-[ <a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a>
-| <a href="https://hdl.handle.net/10012/16059">hdl</a>
-| <a href="https://bndl.org/mmath.html">http</a>
-]
-</small>
-</dt>
-<dd>
-<a href="https://bndl.org">Amin Bandali</a><br />
-<em><abbr title="Master of Mathematics">MMath</abbr> Thesis,
-University of Waterloo, David R. Cheriton School of Computer Science,
-July 2020.</em>
-</dd>
-</dl>
-
-<h3>Talks</h3>
-
-<dl>
-<dt>Jami and how it empowers users
-<small>
-[ <a href="https://p.bndl.org/bandali-jami-libreplanet-2021.pdf">pdf</a>
-(<a href="https://p.bndl.org/bandali-jami-libreplanet-2021-with-notes.pdf">with
-notes</a>)
-| <a href="https://bndl.org/libreplanet-2021.html">http</a>
-]
-</small>
-</dt>
-<dd>
-<a href="https://bndl.org">Amin Bandali</a><br />
-<em>Presented at the LibrePlanet 2021 Conference, March 20, 2021.</em>
-</dd>
-
-<dt>The Magic of Specifications and Type Systems
-<small>
-[ <a href="https://p.bndl.org/cucsc-2017-slides.pdf">slides</a>
-| <a href="https://p.bndl.org/eecs4080-poster.pdf">poster</a>
-]
-</small>
-</dt>
-<dd>
-<a href="https://bndl.org">Amin Bandali</a>,
-<a href="https://github.com/cipher1024">Simon Hudon</a>,
-<a href="https://www.eecs.yorku.ca/~jonathan/">Jonathan S. Ostroff</a><br />
-<em>Slides presented at the Canadian Undergraduate Computer Science
-Conference 2017, University of Toronto, Canada, June 15–17, 2017.<br />
-Poster presented at the Lassonde Undergraduate Summer Student Research
-Conference, York University, Toronto, Canada, August 15, 2017.</em>
-</dd>
-
-<dt>Introducing YULUG</dt>
-<dd>
-<a href="https://bndl.org">Amin Bandali</a><br />
-<em>Slides introducing YULUG — (GNU/)Linux User Group at York
-University — presented at a Computing Students Hub (CSHub) tech
-talk at York University, Toronto, Canada, February 12, 2015.</em>
-</dd>
-</dl>
-
-<h2>Work & Research Experience</h2>
-
-<dl>
-<dt>Savoir-faire Linux</dt>
-<dd>fall 2020–present | Free Software Consultant | Consultant en
-logiciel libre</dd>
-<dd>
-<dl>
-<dd>I am part of the Jami core development team at Savoir-faire Linux,
-where I work on various parts of Jami as a Free Software Consultant.
-These include working on and maintaining the GTK+-based jami-gnome
-client application written in C++ and C, and packaging Jami for
-various GNU/Linux distributions and other platforms. I also serve as
-a community liaison between the Jami core team and the wider free
-software community around Jami, with the goal of helping facilitate
-the communications and relations between the two.</dd>
-</dl>
-</dd>
-
-<dt>Free Software Foundation (FSF)</dt>
-<dd>spring 2020 | Intern</dd>
-<dd>
-<dl>
-<dd>Working with the FSF tech team in a sysadmin role on a variety of
-tasks including installation of the Sourcehut free software forge on
-the FSF infrastructure for evaluation for the FSF forge project, as
-well as a series of enhancements
-for <a href="https://www.gnu.org">www.gnu.org</a>.</dd>
-</dl>
-</dd>
-
-<dt>Cheriton School of Science, University of Waterloo</dt>
-<dd>winter 2018–spring 2020 | TA, IA, RA <sup>[*]</sup></dd>
-<dd>
-<dl>
-<dd>SE 465 (Software Testing and Quality Assurance): TA in winter
-2020</dd>
-<dd>SE 212 (Logic and Computation): <a href="se212-f19.html">IA in
-Fall 2019</a>, TA in fall 2018</dd>
-<dd>SE 463 (Software Requirement Specification and Analysis): TA in
-spring 2019 and 2018</dd>
-<dd>CS 136 (Elementary Algorithm Design and Data Abstraction): TA in
-winter 2018</dd>
-</dl>
-</dd>
-<dd><small>[*]: Teaching Assistant (marking exams and assignments),
-Instructional Apprentice (holding tutorials and marking), Research
-Assistant (doing research for/with supervisor)</small></dd>
-
-<dt>Department of Electrical Engineering & Computer Science, York
-University</dt>
-<dd>fall 2017 | Teaching Assistant</dd>
-<dd>
-<dl>
-<dd>EECS 1012 (Net-Centric Introduction to Computing): TA in fall
-2017, running labs and marking labs and exams</dd>
-</dl>
-</dd>
-
-<dt>Software Engineering Lab, York University</dt>
-<dd>
-<dl>
-<dt>summer 2017 | Research Assistant</dt>
-<dd>Worked on an implementation
-of <a href="https://bertrandmeyer.com/2014/12/07/lampsort/">Lampsort</a>
-in Eiffel. Extended
-the <a href="https://svn.eecs.yorku.ca/repos/sel-open/mathmodels/">mathmodels</a>
-library, implementing a <code>rational</code> class for working with
-arbitrarily large rational numbers.</dd>
-</dl>
-</dd>
-<dd>
-<dl>
-<dt>summer 2016 | Research Student</dt>
-<dd>Worked on <em>Literate Unit-B</em>, 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), decoupled the logic module and used it to build
-<em>Unit-B Web</em>, a web interface using Literate Unit-B to do
-predicate calculus proofs. Unit-B Web, also written in Haskell,
-supports the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span>
-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.</dd>
-<dd>Separated Literate Unit-B's type checker from its parser in a
-large refactoring, allowing easier substitution of other type checking
-algorithms, and in preparation for implementing subtyping.</dd>
-</dl>
-</dd>
-
-<dt>Lotek Wireless Inc.</dt>
-<dd>
-<dl>
-<dt>summer 2016 | Software Developer</dt>
-<dd>Designed and developed an Employee Portal web application in C#
-and the MVC framework, used by employees for accessing various data
-catalogs and archives.</dd>
-</dl>
-</dd>
-<dd>
-<dl>
-<dt>summer 2015 | Computer Programmer</dt>
-<dd>Designed and implemented various applications in C# and C for
-analyzing and testing a satellite pass prediction algorithm for
-predicting the pass windows of Argos satellites, for scheduling send
-times of data collected by the company's wildlife tracking
-products.</dd>
-</dl>
-</dd>
-
-<dt>Athlete Builder</dt>
-<dd>
-<dl>
-<dt>2013–2014 | Software Developer</dt>
-<dd>Developed the Backend of Athlete Builder platform in C# and
-MVC.</dd>
-<dd>Key role in development of the platform core.</dd>
-<dd>Developed the alpha version of Athlete Builder Android application
-in Java.</dd>
-</dl>
-</dd>
-</dl>
-
-<h2>Skills</h2>
-<dl>
-<dt>Programming languages</dt>
-<dd>C, C++, Haskell, Emacs Lisp, Guile Scheme, Python, Eiffel, Bash,
-C#, Java, JavaScript</dd>
-<dt>Tools</dt>
-<dd>GNU Emacs, Git, Alloy, TLA<sup>+</sup>,
-ProB, <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span>, continuous
-integration systems</dd>
-<dt>Platforms</dt>
-<dd>GNU/Linux distributions, including Trisquel, GNU Guix, Debian</dd>
-<dt>Languages</dt>
-<dd>Persian (mother tongue), English (native proficiency; IELTS: 9.0),
-French (beginner)</dd>
-</dl>
-
-<h2>Community Service</h2>
-<dl>
-<dt>EmacsConf conference</dt>
-<dd>
-<dl>
-<dt>2019–present</dt>
-<dd>Chief organizer and maintainer of conference infrastructure,
-including the streaming servers.</dd>
-<dt>2015</dt>
-<dd>One of the organizers and in charge of setting up and maintaining
-vital pieces of infrastructure.</dd>
-</dl>
-</dd>
-<dt>Computer Science Club (CSC) of the University of Waterloo</dt>
-<dd>Served as the CSC System Administrator in Winter and Spring 2020.
-Present member of the CSC Systems Committee, overseeing and
-maintaining a large fleet of GNU/Linux servers for CSC members, as
-well as running the CSC mirror for free software projects.</dd>
-<dd>Notable projects
-include <a href="https://mailman.csclub.uwaterloo.ca/pipermail/csc-general/2020-July/000837.html">launching
-the CSC web IRC client</a> as part of an effort in bringing modern
-user freedom- and privacy-respecting communication tools to club
-members.</dd>
-<dt>Free/libre software contributions</dt>
-<dd>Co-maintainer
-of <a href="https://www.gnu.org/software/gnuzilla/gnuzilla.html">GNUzilla
-and IceCat</a>, the GNU version of the Mozilla suite and the Firefox
-browser respectively.</dd>
-<dd>Maintainer
-of <a href="https://www.gnu.org/software/emacs/erc.html">ERC</a>, the
-powerful, modular, and extensible IRC client distributed with GNU
-Emacs.</dd>
-<dd>Committer and regular contributor
-to <a href="https://www.gnu.org/software/emacs/emacs.html">GNU
-Emacs</a> and <a href="https://guix.gnu.org">GNU Guix</a>.</dd>
-<dd><a href="https://www.gnu.org/people/webmeisters.html#bandali">GNU
-webmaster</a>
-and <a href="https://savannah.gnu.org/maintenance/SavannahHacker/">GNU
-Savannah hacker</a>.</dd>
-<dt>Volunteer work</dt>
-<dd>
-<dl>
-<dt>spring 2013 | Application Developer for VONICAL Inc.</dt>
-<dd>Worked on development of the Employment Accessibility Resource
-Network (EARN) portal using the Anahita social networking platform,
-written in PHP and running on GNU/Linux.</dd>
-<dt>winter 2013 | Mobile & Web Developer for Hire Works Inc.</dt>
-<dd>Worked on a variety of web and mobile development projects for
-Hire Works.</dd>
-<dt>summer 2012 | Web Developer for St. Brigid's Summer Camp</dt>
-<dd>Redesigned and revamped the codebase for the photo gallery section
-of the camp's website in PHP and JavaScript.</dd>
-</dl>
-</dd>
-</dl>
-</body>
-</html>