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 using the identity function in the metalanguage, Lam (λx. x) : Term.

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 modelled in CBPV with thunks using the usual CBV translation. Can CBPV model a CBN language with constructs that explicitly evaluate eagerly?

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 uticaria (itchiness). The antihistamines you can get for allergies are H₁-receptor antagonists, meaning they bind to the H₁ receptors and prevent histamine from triggering them, as well as producing some sort of antagonist effect (?). Simons and Simons 2011 is a pretty good overview of how it works.

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 moment, and my default font of choice is currently Fira Code.

Seven Years of Thulium

I’ve now been running my personal server, Thulium, for seven years and four-and-a-half months, and three of those years have elapsed since my previous post. Not much had changed in those intervening years until very recently, so I thought I’d map them out here.

The Philadelphia Restaurant Graveyard

This was originally an updating post on types.pl.

Since moving to Philadelphia in 2022, a number of beloved restaurants I’ve discovered have since closed in my mere years here, so I’m keeping this table as a remembrance of restaurants past.

HTML Day 2025 ❇️