Varphi
Built by Hassan El-Sheikha, undergraduate, under my supervision
A description language and debugger for Turing machines. My CSC363 students use it to write and step through their machines. Published at WCCCE ’25 and ’26.
Projects
Two kinds of work live here: lessons I built that you can try right now, and tools my student teams built under my supervision. On the second kind, the label on each card says who did what.
Interactive lessons
Every exercise asks for your answer before it shows you anything, and a wrong answer gets feedback on the mistake it most likely came from. Plain pages, no accounts; progress stays in your browser. All four lessons.
Quantifier Gym
“For all” and “there exists”: why swapping their order changes the meaning. Play the ε–δ definition of a limit as a two-player game, then write the proof and let the page attack it.
Nearest Neighbours
Drag a point, change k, and watch the decision boundary redraw. Then step inside a cube and see why “nearest” stops meaning much in high dimensions.
Counting Steps
A run costs a number; a program costs a function. Count steps, plot the worst case, and play big-O as a game against a challenger. Built from my data-structures lecture.
Mechanical Moves
Turing machines in the notation my computability students use, stepped one move at a time. Write the shortest program for n + 1, then make one that never halts.
Built by student teams I supervised
Graph isomorphism on a quantum annealer
M. Akhtar, D. Wrona, R. Chowdhury, one undergraduate and two graduate students; I derived the formulations and directed the project
Three graph-isomorphism formulations, each refining the last, run on D-Wave’s Advantage2. The paper measures how much of the work classical pruning does before the annealer starts.
Tiny Proof
Seven-student team, January–April 2025; I defined the problem and what counted as a working result
An AI-assisted prover for Lean 4 that extends DeepSeek-Prover-V1.5 with a tree search over swappable heuristics.
Transformer Visualizer
Five-student team, under my mentorship
A teaching tool for looking inside a language model, stage by stage, across the layers and attention heads of GPT-2 and BLOOM-560M.
Querying graph databases
Four-student team, CSC492, Winter 2026
A survey of how graph database systems answer multi-hop queries, with reproducible benchmarks of two published techniques and their limitations written down.
Vaught’s conjecture
Summer research student, NSERC Undergraduate Student Research Award, 2026
Organizing and streamlining the recent results on a classic open problem in model theory, which also has a computability-theoretic equivalent.