Bob Atkey

@eigil @mkerjean No. Even if you anonymise the submission, HotCRP will show the PC your name.

@cahollenbeck@mastodon.scot When I have to make videos I do think "Damn it, I'm a doctor, not an actor"

The deadline for the eleventh Mathematically Structured Functional Programming workshop has been extended to 7th May.

Submission site: https://submissions.floc26.org/msfp

Main site: https://msfp-workshop.github.io/msfp2026/

We are looking for long and short papers and interesting talks on applying mathematics to programming.

@mkerjean@lipn.info

@counting_is_hard All I ever wanted, all I ever needed, is here in Ass(K)

I tried to find out if Edinburgh City Council had an API for swimming pool times and found this dormant github repository with a grim final commit message

https://github.com/edinburghcouncil/datasets

@lenary@types.pl albatross colour

As idle as a painted term upon a painted turnstile

Correction: this is the *eleventh* MSFP. I was confused by the fact that it happens every two years!

The Twelfth workshop on Mathematically Structured Functional Programming now has a webpage: https://msfp-workshop.github.io/msfp2026/ . We are affiliated with FSCD at FLoC 2026 in Lisbon this July.

@mkerjean@lipn.info and I are still getting some things organised, but now is the time to start thinking about your mathematically structured submissions!

@chrisamaphone What do you mean by resource semantics? The logical relations indexed by a monoid?

@cbaberle @chrisamaphone Nicely written! I've not seen anyone explore the ordered case before. There's also Linear Plotkin-Abadi logic ( https://arxiv.org/abs/cs/0611004 ) that axiomatises parametricity reasoning for a linear type system. Their motivation was to use linear types as an abstract domain theory though. I did a short example of linear types + logical relations to prove that linear functions from lists to lists are always permutations: https://github.com/bobatkey/sorting-types/blob/master/agda/Linear.agda . The original idea for this was from @pigworker The was later (briefly) written up in a more general form for any semiring-graded system by @mudri and me: https://bentnib.org/context-constrained.pdf and also in a slightly different way by Bernardy and Abel: https://dl.acm.org/doi/10.1145/3408972