Today at ASPLOS Chengsong Tan will present our work with @wicko3.bsky.social on mechanical formalisation of CXL.cache - check out the paper! www.doc.ic.ac.uk/~afd/papers/... #CXL

Check out our work on Formalising CXL Cache Coherence, which Chengsong Tan will present at @ASPLOSConf next week (joint with @wicko3.bsky.social) www.doc.ic.ac.uk/~afd/papers/...

Tfw you forget whether you're playing Tetris or Wordle...

My bank:

Was delighted to have Jianyi Cheng, my former PhD student (joint with @wicko3.bsky.social), now Assistant Professor at @edinburgh-uni.bsky.social Informatics, visit for lunch and technical discussions today. He's doing great work - anyone looking to do a PhD in Scotland - would recommend!

How does a Roman write 9 in Verilog? I don’t care.

Three parking signs in close proximity in Cambridge. Pic 1: clearly non-electric vehicles are not allowed. Pic 2: clearly non-electric vehicles are allowed. Pic 3: ???

Here's a short blog post about an upcoming #PLanQC paper on "QuteFuzz", a new tool built by Ilan Iwumbwe and Benny Liu for fuzz-testing quantum compilers using randomly generated circuits (paying particular attention to subcircuits and control flow) johnwickerson.wordpress.com/2024/12/18/f...

Lindsey’s zine is indeed well worth a read — a thought-provoking introduction to “choreographies” as a method for correct-by-construction concurrent programming.

Lindsey Kuper's* group has produced this fantastic zine on choreographic programming that folks should definitely check out: decomposition.al/blog/2024/12... (* can't seem to find Lindsey here but please tag if you know the handle)

Formally Verified Hardening of C Programs Against Hardware Fault Injection hal.science/hal-04818801 gricad-gitlab.univ-grenoble-alpes.fr/certicompil/...

Program correctness and incorrectness are not just two sides of the same coin; they're two faces of the same cube! johnwickerson.wordpress.com/2024/12/04/t...

I reckon I'm old enough to pontificate confidently on topics I know nothing about, so here's my blog post all about ... the UK's rules on income tax! johnwickerson.wordpress.com/2024/11/26/f...

"A Verified Foreign Function Interface between Coq and C", by me, Kathrin Stark and Andrew W. Appel will appear at POPL 2025! www.cs.princeton.edu/~appel/paper... this is the culmination of years of research (and most of my grad school work), so I'm excited to see it finally published! 🎉

Big thanks to Prof Danilo Mandic for an inspiring “Meet the Profs” seminar today. He explained how he has applied his expertise in signal processing to such varied domains as financial trading, heart monitoring, and sleep apnoea.

The recording of our POPL song, "Reviewing for Publication", is now available: https://www.youtube.com/watch?v=Hyaeg7C4XsI

["Girls in white dresses with blue satin sashes"; "Snowflakes that stay on my nose and eyelashes"; "Silver white winters that melt into springs"] -- These are a few of my favourite strings.

“Penguin Random House” sounds more like a what3words reference than a publishing company.

If #juliadonaldson were an academic...

I wrote this on my son’s changing mat to stop me using it upside-down, but it’s not as helpful as I’d hoped...

When building some hardware the HLS way There's no task more vital or bigger, Than figuring out, for each step of the clock, Which gates are the next ones to trigger.

The “Updated just now” message in the iOS Mail app is a poor #UX decision. It should give me the actual time of the last update. Otherwise I can’t judge whether the message itself is out of date!

@ETAPSconf should inaugurate a “programming pearls” track and call it “ESOP fables”.

I feel a bit sorry for car drivers who get a ticket for driving past this point. I don’t think the signs are clear enough, e.g. “bus gate” is an unfamiliar term. Needs a big ⛔️ sign saying “except buses”, right? @camcitco @CB1_Development @StationaryRoad

Apparently too many people are putting duck feathers on the seats at Stansted Airport.

Standing in the @British_Airways check-in at @HeathrowAirport. One officer spent 84 seconds checking in one passenger, then 16 seconds waiting for the next passenger to wake up and amble over to the desk. 1/3

Four errors/inconsistencies on a single sign is quite impressive!

#UXFail on the Tube: Default state of ticket barrier is "CLOSED", which suggests "don't even try". Perhaps "READY" would be more inviting?

Hello!

Beautiful talk by Justin Hsu, visiting from Cornell, on how to deploy a linear type system to keep track of the rounding errors introduced by floating-point arithmetic!

Big thank you to Eleonora Giunchiglia @e_giunchiglia for a fascinating “Meet the Profs” talk at @imperialeee about her research into compliant-by-construction ML models!

A good day for folks who like runs of numbers!

Delighted to have our first “Meet the Profs” seminar of the term, featuring Ayush Bhandari (@AB2World) who showed us how to extract a useful signal just from the noise of quantisation! Simultaneously mind-blowing and beautifully explained. @imperialeee

Did I just wake up after a 400-year nap?

Who checks the equivalence checkers? My PhD student Michalis Pardalos will be speaking at DVCon next month about fuzz-testing formal equivalence checkers, a joint project with Ally Donaldson, Emi Morini, and Laura Pozzi. johnwickerson.wordpress.com/2024/09/10/w...

@niclane7 thanks for an inspiring talk at the NANDA workshop yesterday. You spoke of centralised networks where raw data is sent along the links, and federated networks where models are sent along the links. Can I think of …

Here's a short preview of a paper that Quentin Corradi, my PhD student with George Constantinides, will be presenting in the FUZZING'24 workshop at ISSTA next week... johnwickerson.wordpress.com/2024/09/09/a...

I'm delighted that @LukeGeeson's work on "mix testing" of compilers will appear at #OOPSLA2024 (joint with Brotherston, Dijkstra, @afd_icl, Smith, @Tyler_UCSC, and myself). Here's a blog post that gives a short introduction to the project:...

A lovely tribute to one of my favourite lecturers as an undergraduate: https://www.cst.cam.ac.uk/news/computer-scientist-whose-technology-helped-millions-prove-their-identity

#include <assert.h> int main() { int x = 5; assert (0 <= x < 3); //this passes! }

In case anybody else is interested in cycling from King’s Cross to the South Kensington campus of Imperial College London: https://johnwickerson.wordpress.com/2024/05/11/cycling-from-kings-cross-to-imperial-college-london/

Huge congrats to Yann Herklotz (@ymherklotz) for successfully defending his PhD thesis today, all about his proven-in-Coq high-level synthesis tool. And enormous thanks to George Constantinides (@gconstantinides) and Xavier Leroy for their thoughtful and thorough examining.

Which compiler optimisation is this one again?

“Hello, I’d like to return this bicycle please. The axles aren’t in the centre of the wheels.”

The talks from the #POPL2024 workshop on the "Future of Weak Memory" are now available as a YouTube playlist! https://www.youtube.com/playlist?list=PLyrlk8Xaylp6u1S3R6gH0W9dkxJhH4B9W

I’m delighted that @ymherklotz’s work to add hyperblock scheduling to his verified HLS tool will be presented at #PLDI2024. Here’s a short preview of the paper… https://johnwickerson.wordpress.com/2024/03/01/verified-high-level-synthesis-now-with-hyperblocks/

“23-19! We have a 23-19 over here!”

I wrote up some thoughts about a curious alternative to Incorrectness Logic https://johnwickerson.wordpress.com/2024/02/15/what-is-the-other-incorrectness-logic/

GitHub advice from my local leisure centre

Sulphur hexafluoride is not to be smoked in this taxi.