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