Regretfully, the petition to remove #LGBT content from the #UK curriculum has 197,100 signatures.

The counter petition asking for that content to remain, is rapidly gaining ground. It now has 78,919 signatures!

Pls sign the counter petition if able. British citizens & UK residents have the right to sign. Pls boost otherwise!

Link to official petition to UK Gov & Parliament: Do not remove LGBT content from the Relationships Education curriculum

petition.parliament.uk/petitio

I stupidly decided to upgrade my emacs version. Then Agda (2.6.2) started complaining about cl package being deprecated. Trying to upgrade my version of Agda to 2.6.4 lead me to reinstall Haskell, Cabal, and Agda.

THEN I FIND OUT in the new Agda version previous proofs involving rewrites were broken.

So I've spent 4 hours arsing about to get back to running normally and now I'm not sure I cba working on my normalisation proof.

Children

Why are they drawn to a clean room like painters to a blank canvas?

RT @luismbat@birbsite

Who would have thought that adding a Sierpinski Triangle Fractal as musical notes would actually sound good!😅

#UK folks, there's a petition to keep protection of transgender people in the equality act by not amending it.

It's pretty scary being #trans in this country at the moment, and we could use your help to protect our rights. #Queer folks and #lgbtq friends and allies, please support.

Feel free to share broadly/openly with others. Steal, boost, repost your own. Let's get 100k signatures, please.

petition.parliament.uk/petitio

Looks like I should read the Lamping paper "an algorithm for optimal lambda calculus reduction" instead.

Based on the unary arithmetic example it looked like I could encode graph rewriting using Bove-Capretta, but then weird arrangements of combinators turned up and I have no idea what is going on.

I want to understand some really cool tech (github.com/Kindelia/HVM) but I’m not getting the interaction nets stuff.

Had a quick read over the Symmetric Interaction Combinators paper, it’s just not clicking for me.

As is alway the case in academia, I'm looking forward to term ending so that I can get some work done over the holidays.

@JacquesC2 are you in the office on Friday? I wanted to chat with you about partial evaluators, if you are ok with that.

I’ll be taking part in my first strike action now that UCU has announced strike days.

Just learned about interpolated search at the weekend, and then I found interpolated binary search.

A thing that made me grumpy about the Other Place was that replies were usually from people I didn't know telling me I was talking rubbish. To be fair, I often am talking rubbish, but so far here it's been constructive efforts at telling me I'm talking rubbish.

I have been on the Internet long enough to know it won't last but I'm going to enjoy it while it does :).

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.