CS PhD student @ UPenn [he / they]
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.
More …
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!
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.
More …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.
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?
More …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.
More …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.
More …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.
More …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.
More …This is a table similar to Wikipedia’s zhuyin table, but with slightly different sorting and an example for each possible combination of initials and finals.
More …
