Jonathan Chan

Boston

I’m in Boston!

Little LaTeX Pearls

Over the course of the LaTeX-typeset papers I’ve written during grad school, there are some tricks and macros I’ve carried with me all throughout. Here’s a small catalogue of some of the generally applicable ones.

Why I don’t use generative AI

As someone who categorically so far refuses to use generative AI and LLMs for code in particular, I’m increasingly becoming the odd one out among my peers in academia. I don’t have the persuasive power nor the actual arguments against using LLMs to convince them otherwise, but because I’m now officially in the minority at my workplace, I feel the need to explain why I personally don’t use LLMs.

Paper Ephemera

U+237C ⍼ is Azimuth

Part 1 · Part 2 · Part 3 · Part 4 · Part 5 ← you are here One year ago, on 28 February 2025, Wikipedia user Moyogo updated the page for Angzarr with a citation to the type foundry H. Berthold AG’s 1950 symbol catalogue listing ⍼ as Azimut, Richtungswinkel, or “azimuth”, “direction angle”. Mystery solved!

Timeline of songs in Heated Rivalry

This was originally a Tumblr post. Spotify has an official Heated Rivalry playlist of all the credited songs, but I wanted to create a subset of this playlist with only the songs that we can actually hear clearly hear (non-diegetically) in the show, so I’ve catalogued the songs here with details on where and when they appear.

HOAS using CBPV with dependency tracking

Higher-order abstract syntax (HOAS) uses binding in the ambient metalanguage to represent binding in the object language. For example, if we define Terms of the object language as a type in the metalanguage, we might give functions of the lambda calculus (our object language) the type Lam : (Term → Term) → Term. The identity function in the object language is then represented by this constructor…

Modelling laziness with a little bit of strictness

Evaluation of the lambda calculus is a spectrum from strictness, or call by value (CBV), to laziness, or call by name (CBN). Paul Levy’s call by push value (CBPV) subsumes both CBV and CBN. A form of this sentence is in the introduction of every paper on CBPV. CBPV also subsumes other points along the spectrum. A CBV language with explicit thunking constructs to delay computation lazily can be…

Antihistamines

This was originally a really long toot. I’ve been looking at papers on antihistamines and what makes them work better like, molecularly, not just doing clinical trials and seeing what happens. As a primer, allergens trigger the release of histamines in the body, which then bind to various histamine receptors, and the H₁ receptors are the important ones that trigger rhitinis (runny nose, etc.) and…

Nice mono fonts I don’t use

There are a lot of nice monospaced code-writing fonts that I don’t use. For some of them, there are tiny, specific nitpicks about why I don’t use them. My use case is writing code with a lot of Unicode, like in Lean or Agda, writing Markdown with a lot of Unicode because I can, and having a terminal that looks nice. For reference, I’ll be comparing a snippet of a proof state I have open at the…