Ben's Site

I’m currently a PhD student in mathematics (started in May 2023) at Western University supervised by Chris Kapulkin. I graduated from the University of Toronto with an MSc in mathematics in August 2022 and from the University of Western Ontario with a BESc in Computer Engineering and a BSc with Honours Specialization in Mathematics in April 2021.

Since fall 2024 I’ve been a member of the Early Music Studio at Western under the direction of Joe Lanza (Baroque performance) and Borys Medicky (performance and harpsichord). In summer 2026 I attended TBSI, studying with Charlotte Nediger and Olivier Fortin (among many others). Some music things of mine (mostly Baroque) are hosted on this site, see here.

I can be reached at first name dot last name at uwo dot ca.

Interests

My main interests are in (homotopy) type theory and formalization of mathematics. I’m also interested in higher category theory, homotopy theory, applications of category theory, programming languages, computer architecture, and image processing.

TA

  • Fall 2024: Math 2155 (UWO)
  • Fall 2024: Math 2151 (UWO)
  • Winter 2024: Math 1600 (UWO)
  • Fall 2023: Math 2155 (UWO)
  • Fall 2023: Calculus 1500 (UWO)
  • Summer S 2022: Math 224 (UofT)
  • Summer F 2022: Math 224 (UofT)
  • F/W 2021: Math 137 (UofT)

Projects

See my stagit instance for personal programming projects.

Reports/Notes

Hofmann Revisited

An in-progress note with a modern (and detailed) presentation of Hofmann’s paper interpreting type theory in LCCCs for use in the proof of Uemura’s paper on representable map categories.

Chasing Databases: The Theoretical Evolution of Data Migration

Completed as my MSc summer project at UofT under the supervision of Yun William Yu. This report summarizes three of the major developments by Spivak et. al in categorifying relational databases and gives some justification of each new development.

Seminars

Past Projects

  • agda-unimath: Working towards formalizing the algebraic small object argument.
  • Coq-HoTT: Formalizing Wärn’s zigzag construction in Rocq with Thomas Thorbjørnsen.
  • ABL Temporal Bone Segmentation: Plugin for 3DSlicer to automatically segment CT scans of the temporal bone.
  • ABLInfer: Library and command-line tool for dispatching medical images to segmentation and registration toolkits, primarily using Docker; written for the “ABL Temporal Bone Segmentation” plugin.

Links

Site Info

This site is static and 100% JavaScript free. It’s built using the Zine static site generator with a customized version of the plague (Hugo) theme. My stagit instance is generated using a mildly modified version of Oscar Benedito’s stagit fork. No part of this site, including supporting scripts, was written, developed, checked, etc. by generative AI/LLMs.