wen @cyrridven@computerfairi.es

proving soundness of an operational correspondence is weird, 'cuz all the cases are like "well, clearly no other rule applies, look!"

the difference between me—a white person who sounds english—and my partner—a latine person with a slight accent—calling ANY danish authority is palpable.

they get unhelpful people who are sticklers for the rules, get told the person they need to talk to is out or VERY busy, or that the relevant computer system is down and to wait for a callback which never comes.

when calling only a couple minutes later for the same issue, I get helped IMMEDIATELY by friendly people.

why does "army of lovers" lead to "ace of bass" recs on youtube? that's a pretty big step from "very gay" to "very fash"?

my physiotherapist has tasked me with doing what I can only assume are bored flying kicks

suggestions for non-ableist alternatives to "blind" in the comments please

single-blind peer review is worse than unblinded-peer review send tweet

My favourite thing about being an academic is knowing that at some undefined point in the future, I'll probably have to change careers and start from scratch.

danish government helplines be like "pick 2 for english" and then proceed to say everything in danish, except for the number 6

with all the different context switching commands, I keep creating branches called "remove" and switching to an ocaml version with docs

thanks to @ulfnorell@twitter.com for helping out with the reflection hooks!

we updated schmitty and now she can do this

agda open without using considered harmful send tweet

I do believe that establishes the precedent that "omega underline" is pronounced as "with type constructors"

if "system F omega underline" can be a well-established point on the lambda cube, I don't want any more negative feedback on my use of emoji in papers

Little known fact! In Denmark, it takes two days for an email to arrive. Ethnographers theorise this is due to the government's contract with Microsoft, but so far this hasn't been confirmed.

Checking first-order languages like:

check Γ BOOL (forAll body) =
check (BOOL ∷ Γ) BOOL body ∨
check (INT ∷ Γ) BOOL body

my partner banned me from dancing while handling a knife in the kitchen, which... fair, that's probably a good call.

anyway, after spending a good amount of time writing it, turns out i don't really need it 🤷🏻‍♀️

I love English, it's a great language, and there isn't anything fundamentally wrong with the the language or culture or anything like that, nope, nope, nope... oh what's that screenshot doing there, oh well this is awkward😅

me, after writing an O(n³) algorithm for reversing typing environments: "this is fine"