| 1 | ;;; Copyright © 2019 Amin Bandali <bandali@gnu.org> |
| 2 | ;;; |
| 3 | ;;; This program is free software; you can redistribute it and/or |
| 4 | ;;; modify it under the terms of the GNU General Public License as |
| 5 | ;;; published by the Free Software Foundation; either version 3 of the |
| 6 | ;;; License, or (at your option) any later version. |
| 7 | ;;; |
| 8 | ;;; This program is distributed in the hope that it will be useful, |
| 9 | ;;; but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 10 | ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
| 11 | ;;; General Public License for more details. |
| 12 | ;;; |
| 13 | ;;; You should have received a copy of the GNU General Public License |
| 14 | ;;; along with this program. If not, see |
| 15 | ;;; <http://www.gnu.org/licenses/>. |
| 16 | |
| 17 | (define-module (bandali pages) |
| 18 | #:use-module (bandali prefs) ; my-* |
| 19 | #:use-module (bandali theme) ; base-layout |
| 20 | #:use-module (bandali utils) ; aa |
| 21 | #:use-module (haunt html) ; sxml->html |
| 22 | #:use-module (haunt page) ; make-page |
| 23 | #:use-module (ice-9 match) ; match-lambda |
| 24 | #:export (static-page |
| 25 | index-page |
| 26 | license-page |
| 27 | contact-page |
| 28 | cv-page |
| 29 | se212-f19-page)) |
| 30 | |
| 31 | (define* (static-page title file-name body copy #:key license?) |
| 32 | (lambda (site posts) |
| 33 | (make-page file-name |
| 34 | (base-layout site body #:title title #:copy copy |
| 35 | #:license-page? license?) |
| 36 | sxml->html))) |
| 37 | |
| 38 | (define (index-material site posts) |
| 39 | `((h1 (@ (style "font-size: 0;")) |
| 40 | "Amin Bandali") |
| 41 | (p (@ (style "margin-top: 0;")) |
| 42 | "Hi, I’m " |
| 43 | ,(aa "Amin Bandali" "images/bandali-with-rms.jpg" |
| 44 | "photo of bandali with rms wearing a " |
| 45 | "“pay cash don’t be tracked” pin") |
| 46 | ". I’m a graduate student at " |
| 47 | ,(aa "WatForm" "https://watform.uwaterloo.ca") |
| 48 | " at University of Waterloo, supervised by " |
| 49 | ,(aa "Dr. Nancy Day" "https://cs.uwaterloo.ca/~nday/") |
| 50 | ". The main goal of my research is improving " |
| 51 | (strong "software and systems reliability") |
| 52 | " through application of " (em "formal methods") ".") |
| 53 | (p "My research at WatForm focuses on formal logic, model " |
| 54 | "checking, and verification. I’m also interested in " |
| 55 | "programming languages, theorem provers, and their " |
| 56 | "type systems. You may wish to view my academic " |
| 57 | ,(aa "curriculum vitae" "bandali-cv.html") ".") |
| 58 | (p (@ (class "notice")) |
| 59 | (strong "SE 212 students: ") |
| 60 | "see " ,(aa "here" "se212-f19/") " for slides and other " |
| 61 | "material from the tutorials.") |
| 62 | (p "On the side, I dabble in " |
| 63 | ,(aa "Lean" "https://leanprover.github.io") " and enjoy " |
| 64 | ,(aa "hacking" "https://stallman.org/articles/on-hacking.html") |
| 65 | " on " |
| 66 | ,(aa "Elisp" |
| 67 | "https://www.gnu.org/software/emacs/manual/elisp.html") |
| 68 | ". I’m a " ,(aa "Free Software" |
| 69 | "https://www.gnu.org/philosophy/free-sw.html") |
| 70 | " activist, a GNU " |
| 71 | ,(aa "maintainer" "https://www.gnu.org/people/#bandali") |
| 72 | " and " |
| 73 | ,(aa "webmaster" |
| 74 | "https://www.gnu.org/people/webmeisters.html#bandali") |
| 75 | ", and an " ,(aa "associate member" |
| 76 | "https://www.fsf.org/associate/") |
| 77 | " of the " ,(aa "FSF" "https:///www.fsf.org" |
| 78 | "Free Software Foundation") |
| 79 | ". I co-host the " ,(aa "Emacs.el" "https://emacsel.com") |
| 80 | " podcast with " ,(aa "Daniel Gopar" "https://www.pygopar.com") |
| 81 | ", and organize " ,(aa "EmacsConf" "https://emacsconf.org") |
| 82 | " with help from many wonderful people. I am also a member of" |
| 83 | " the Systems Committee for the " |
| 84 | ,(aa "CSC" "https://csclub.uwaterloo.ca" |
| 85 | "Computer Science Club of the University of Waterloo") |
| 86 | ".") |
| 87 | (p "See my " ,(aa "contact" "contact.html") " page for how to " |
| 88 | "best reach me.") |
| 89 | (h2 (@ (id "papers")) "Papers") |
| 90 | (dl |
| 91 | (dt "A Comparison of the Declarative Modelling Languages B, DASH, |
| 92 | and TLA" (sup "+") |
| 93 | (small |
| 94 | " [ " ,(aa "pdf" "papers/modre2018-declarative.pdf") " | " |
| 95 | ,(aa "bib" "papers/modre2018-declarative.bib") " ]")) |
| 96 | (dd "Ali Abbassi, " |
| 97 | ,(aa "Amin Bandali" my-url) ", " |
| 98 | ,(aa "Nancy A. Day" "https://cs.uwaterloo.ca/~nday/") ", " |
| 99 | "Jose Serna" |
| 100 | (br) |
| 101 | (em "2018 IEEE 8th International Model-Driven Requirements" |
| 102 | " Engineering Workshop (MoDRE)") |
| 103 | (br) |
| 104 | "Copyright © 2018 IEEE. All Rights Reserved. Sadly.")) |
| 105 | (h2 (@ (id "talks")) "Talks") |
| 106 | (dl |
| 107 | (dt |
| 108 | "The Magic of Specifications and Type Systems" |
| 109 | (small |
| 110 | " [ " |
| 111 | ,(aa "slides" "talks/cucsc-2017-slides.pdf" |
| 112 | "presented at the Canadian Undergraduate Computer Science" |
| 113 | " Conference 2017,\n" |
| 114 | "University of Toronto, Canada, June 15–17, 2017") |
| 115 | " | " |
| 116 | ,(aa "poster" "talks/eecs4080-poster.pdf" |
| 117 | "presented at the Lassonde Undergraduate Summer Student" |
| 118 | " Research Conference,\n" |
| 119 | "York University, Toronto, Canada, August 15, 2017") |
| 120 | " ]")) |
| 121 | (dd ,(aa "Amin Bandali" my-url) ", " |
| 122 | ,(aa "Simon Hudon" "https://github.com/cipher1024") ", " |
| 123 | ,(aa "Jonathan S. Ostroff" |
| 124 | "http://www.cse.yorku.ca/~jonathan/"))) |
| 125 | (h2 (@ (id "projects")) "Projects") |
| 126 | (p "Below are a number of free software projects I have worked " |
| 127 | "on:") |
| 128 | (dl |
| 129 | (dt ,(aa "george-mode" "https://git.sr.ht/~bandali/george-mode")) |
| 130 | (dd "Emacs major mode for editing George files") |
| 131 | (dt ,(aa "alloy-catalyst" |
| 132 | "https://git.uwaterloo.ca/bandali/alloy-catalyst")) |
| 133 | (dd "Framework for performance analysis of Alloy models") |
| 134 | (dt ,(aa "unitb-web" "https://github.com/unitb/unitb-web")) |
| 135 | (dd "Web interface for Unit-B") |
| 136 | (dt ,(aa "tex2png-hs" "https://github.com/unitb/tex2png-hs")) |
| 137 | (dd "Library and CLI for converting TeX and LaTeX to PNG " |
| 138 | "images")) |
| 139 | (h2 (@ (id "notes")) "Notes") |
| 140 | (p "Here are notes about a variety of topics and issues I care " |
| 141 | "about. They’re also available via " |
| 142 | ,(aa `((img (@ (class "feed-icon") |
| 143 | (src "/icon-12px.png") |
| 144 | (alt "subscribe to atom feed"))) |
| 145 | "Atom") |
| 146 | "notes.atom") |
| 147 | " and " |
| 148 | ,(aa `((img (@ (class "feed-icon") |
| 149 | (src "/icon-12px.png") |
| 150 | (alt "subscribe to rss feed"))) |
| 151 | "RSS") "notes.rss") " feeds.") |
| 152 | ,(post-list-table site posts))) |
| 153 | |
| 154 | (define (index-page site posts) |
| 155 | (make-page |
| 156 | "index.html" |
| 157 | (base-layout site (index-material site posts)) |
| 158 | sxml->html)) |
| 159 | |
| 160 | (define license-page |
| 161 | (static-page |
| 162 | "Licensing Information" |
| 163 | "license.html" |
| 164 | `((h1 "License information for " |
| 165 | ,(aa my-domain my-url)) |
| 166 | (p "I strongly believe in " |
| 167 | ,(aa "free culture" |
| 168 | "https://questioncopyright.org/what_is_free_culture") |
| 169 | " and that all creative works everywhere should be " |
| 170 | ,(aa "free" "https://freedomdefined.org/Definition") ".") |
| 171 | (p "Unless otherwise noted material on this site is licensed " |
| 172 | "under the GNU General Public License as published by the " |
| 173 | "Free Software Foundation, either version 3 of the License, " |
| 174 | "or (at your option) any later version. A copy of the " |
| 175 | "license is included at " ,(aa "gpl-3.0.html") ".") |
| 176 | (p "Some resources on free software and licenses:") |
| 177 | (ul |
| 178 | (li ,(aa "What is free software?" |
| 179 | "https://www.gnu.org/philosophy/free-sw.html")) |
| 180 | (li ,(aa "Various Licenses and Comments about Them" |
| 181 | "https://www.gnu.org/licenses/license-list.html")) |
| 182 | (li ,(aa "Proprietary Software Is Often Malware" |
| 183 | "https://www.gnu.org/proprietary/proprietary.html")))) |
| 184 | "2019" |
| 185 | #:license? #t)) |
| 186 | |
| 187 | (define contact-page |
| 188 | (static-page |
| 189 | "Contact Information" |
| 190 | "contact.html" |
| 191 | `((h1 "Contact information") |
| 192 | (p "Email is by far my preferred method of communication. I may" |
| 193 | " be contacted at any of the following addresses (choose the" |
| 194 | " most closely related):") |
| 195 | (ul |
| 196 | (li "bandali@gnu.org") |
| 197 | (li "bandali@uwaterloo.ca") |
| 198 | (li "bandali@csclub.uwaterloo.ca")) |
| 199 | (p "If you want to send me GPG-encrypted mail, you can use my " |
| 200 | ,(aa "public key" "bandali-pubkey.txt") " with the" |
| 201 | " fingerprint " |
| 202 | (code "BE62 7373 8E61 6D6D 1B3A 08E8 A21A 0202 4881 6103") |
| 203 | ".") |
| 204 | (table |
| 205 | (tbody |
| 206 | (tr |
| 207 | (td "IRC") |
| 208 | (td "bandali on " ,(aa "freenode" "https://freenode.net") ", " |
| 209 | ,(aa "moznet" "https://wiki.mozilla.org/IRC") ", and " |
| 210 | ,(aa "oftc" "https://www.oftc.net"))) |
| 211 | (tr |
| 212 | (td "XMPP") |
| 213 | (td ,(aa "bandali@member.fsf.org" |
| 214 | "xmpp:bandali@member.fsf.org"))) |
| 215 | (tr |
| 216 | (td "Matrix") |
| 217 | (td ,(aa "@bandali:matrix.org" |
| 218 | "https://matrix.to/#/@bandali:matrix.org"))) |
| 219 | (tr |
| 220 | (td "Fediverse") |
| 221 | (td ,(aa "@bandali@pleroma.site" |
| 222 | "https://pleroma.site/bandali"))))) |
| 223 | (h2 "Elsewhere") |
| 224 | (p "You may also find me at a few other places online. Stricken" |
| 225 | " through accounts are those I don’t use anymore, unless" |
| 226 | " absolutely necessary.") |
| 227 | (ul |
| 228 | (li ,(aa "bandali" "https://libreplanet.org/wiki/User:Bandali") |
| 229 | " on LibrePlanet") |
| 230 | (li ,(aa "bandali" "https://emacsconf.org/bandali") |
| 231 | " on EmacsConf") |
| 232 | (li ,(aa "bandali" "https://savannah.gnu.org/users/bandali") |
| 233 | " on Savannah") |
| 234 | (li ,(aa "bandali" "https://git.sr.ht/~bandali") |
| 235 | " on Sourcehut") |
| 236 | (li ,(aa "bandali" "https://lobste.rs/u/bandali") |
| 237 | " on Lobsters") |
| 238 | (li ,(aa "bandali" "https://hackage.haskell.org/user/bandali") |
| 239 | " on Hackage") |
| 240 | (li ,(aa "bandali" "https://gitlab.com/bandali") |
| 241 | " on GitLab") |
| 242 | (li ,(aa "bandali" |
| 243 | "https://news.ycombinator.com/user?id=bandali") |
| 244 | " on HN") |
| 245 | (li ,(aa "bandali" "https://www.reddit.com/u/bandali") |
| 246 | " on reddit") |
| 247 | (li (del ,(aa "bandali0" "https://github.com/bandali0") |
| 248 | " on GitHub")) |
| 249 | (li (del ,(aa "bandali0" "https://twitter.com/bandali0") |
| 250 | " on Twitter")))) |
| 251 | "2019")) |
| 252 | |
| 253 | (define cv-page |
| 254 | (static-page |
| 255 | "Curriculum vitae" |
| 256 | "bandali-cv.html" |
| 257 | `((h1 "Curriculum vitae (" ,(aa "PDF" "bandali-cv.pdf") ")") |
| 258 | (table |
| 259 | (tbody |
| 260 | (tr |
| 261 | (td "Site") |
| 262 | (td ,(aa my-domain my-url))) |
| 263 | (tr |
| 264 | (td "Email") |
| 265 | (td "bandali@uwaterloo.ca")) |
| 266 | (tr |
| 267 | (td "Phone") |
| 268 | (td "available upon request via email")))) |
| 269 | (h2 "Education") |
| 270 | (h3 "Master of Mathematics (Computer Science) | 2018–present") |
| 271 | (p "University of Waterloo, Canada") |
| 272 | (p "Supervised by Dr. Nancy Day | GPA: 3.7/4.0 | " |
| 273 | "Expected completion: April 2020") |
| 274 | (p "Research focusing on formal logic, model checking, and " |
| 275 | "verification.") |
| 276 | (h3 "B.Sc. Honours Computer Science | 2013–2017") |
| 277 | (p "York University, Toronto, Canada") |
| 278 | (p "GPA: 7.84/9.0") |
| 279 | (p "Relevant courses: System Specification & Refinement, " |
| 280 | "Software Requirements Eng., Software Design, " |
| 281 | "Operating Systems, Computational Complexity, " |
| 282 | "Design & Analysis of Algorithms.") |
| 283 | (p "Finished first year (2013-14) at " (em "Carleton University") |
| 284 | " with a GPA of 11.0/12.0, then transferred to " |
| 285 | (em "York University") " in Fall 2014.") |
| 286 | (h2 "Publications") |
| 287 | (p "Listed on my " ,(aa "homepage" "/#papers")) |
| 288 | (h2 "Work & Research Experience") |
| 289 | (h3 "Cheriton School of Computer Science, University of Waterloo" |
| 290 | " | 2018–present") |
| 291 | (p "Instructional Apprentice, Teaching Assistant, " |
| 292 | "Research Assistant") |
| 293 | (ul |
| 294 | (li (abbr (@ (title "Logic and Computation")) "SE 212") ": " |
| 295 | (abbr (@ (title "Instructional Apprentice")) "IA") " in " |
| 296 | "Fall 2019, " |
| 297 | (abbr (@ (title "Teaching Assistant")) "TA") " in " |
| 298 | "Fall 2018") |
| 299 | (li (abbr (@ (title ,(string-append |
| 300 | "Software Requirements Specification and " |
| 301 | "Analysis"))) "SE 463") |
| 302 | ": TA in Summer 2019 and 2018") |
| 303 | (li (abbr (@ (title ,(string-append |
| 304 | "Elementary Algorithm Design and " |
| 305 | "Data Abstraction"))) "CS 136") |
| 306 | ": TA in Winter 2018")) |
| 307 | (h3 (abbr (@ (title |
| 308 | ,(string-append |
| 309 | "Electrical Engineering & Computer Science"))) |
| 310 | "EECS") |
| 311 | " Department, York University | Fall 2017") |
| 312 | (p "Teaching Assistant") |
| 313 | (p (abbr (@ (title "Net-Centric Introduction to Computing")) |
| 314 | "EECS 1012") |
| 315 | ": TA in Fall 2017")) |
| 316 | "2019")) |
| 317 | |
| 318 | (define se212-f19-page |
| 319 | (static-page |
| 320 | "SE 212 Material" |
| 321 | "se212-f19/index.html" |
| 322 | `((h1 "Material from SE 212 tutorials") |
| 323 | (p "This page contains slides and other material from " |
| 324 | ,(aa "SE 212 tutorials" |
| 325 | "https://www.student.cs.uwaterloo.ca/~se212/times.html") |
| 326 | " held by me in Fall 2019. " |
| 327 | (del "If you have any questions, concerns, or suggestions " |
| 328 | "about the presented material, please email me at " |
| 329 | "bandali@uwaterloo.ca or come see me during my " |
| 330 | ,(aa "Friday office hours" |
| 331 | "https://www.student.cs.uwaterloo.ca/~se212/personnel.html") |
| 332 | ".")) |
| 333 | (ul |
| 334 | (li "Tutorial 1:" |
| 335 | (ul |
| 336 | (li ,(aa "TUT 101 slides" "se212-t01-101.pdf")) |
| 337 | (li ,(aa "TUT 102 slides" "se212-t01-102.pdf")) |
| 338 | (li ,(aa "Org beamer sources" "se212-t01.org")))) |
| 339 | (li "Tutorial 2:" |
| 340 | (ul |
| 341 | (li ,(aa "Homework 2 q04d solution" |
| 342 | "se212-h02q04d-soln.grg")))) |
| 343 | (li "Tutorial 3: —") |
| 344 | (li "Tutorial 4: —") |
| 345 | (li "Tutorial 5:" |
| 346 | (ul |
| 347 | (li ,(aa "Slides" "se212-t05.pdf")) |
| 348 | (li ,(aa "Org beamer sources" "se212-t05.org")))) |
| 349 | (li "Tutorial 6: —") |
| 350 | (li "Tutorial 7: worked through questions 1–5 of Homework 7") |
| 351 | (li "Tutorial 8: —") |
| 352 | (li "Tutorial 9: —") |
| 353 | (li "Tutorial 10: worked through questions 1–10 of " |
| 354 | "Homework 10"))) |
| 355 | "2019")) |