@bentnib@types.pl

· 5mo ago

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

GitHub

GitHub - edinburghcouncil/datasets: Open Data for Edinburgh

Open Data for Edinburgh. Contribute to edinburghcouncil/datasets development by creating an account on GitHub.

28

0

15

0

Bob Atkey @bentnib@types.pl

· 7mo ago

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!

msfp-workshop.github.io

Mathematically Structured Functional Programming 2026

30

2

25

0

Bob Atkey @bentnib@types.pl

· 5mo ago

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

submissions.floc26.org

9

3

11

0

Bob Atkey @bentnib@types.pl

· 5mo ago

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

3

0

Bob Atkey @bentnib@types.pl

· 6mo ago

As idle as a painted term upon a painted turnstile

3

0

Bob Atkey @bentnib@types.pl

· 5mo ago

Replying to

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

2

0

Bob Atkey @bentnib@types.pl

· 19mo ago

Replying to

@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

arXiv.org

Linear Abadi and Plotkin Logic

We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential types, inductive types, coinductive types and general recursive types. We show that the recursive types satisfy a universal property called dinaturality, and we develop reasoning principles for the constructed ty

6

4

1

0

Bob Atkey @bentnib@types.pl

· 19mo ago

Replying to

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

0

1

0

Bob Atkey @bentnib@types.pl

· 5mo ago

Replying to

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

0

Bob Atkey @bentnib@types.pl

· 6mo ago

Replying to

@lenary@types.pl albatross colour

0