Lindsey Kuper / is on Nostr

CSE assistant professor at UC Santa Cruz (PL / distributed systems / verification). Made in Iowa. Nearly 100% biodegradable.

searchable

Last Notes

2024-07-08 05:59:11

- reply

it means "me and only me"

2024-05-26 15:59:41

Seeing people toot that they're bummed about how little coverage there was of the Voyager 1 fix, and I want to reply WE'RE HAVING A KEYNOTE TALK AT @npub1nzv…d8m0 ABOUT IT!!!!!!! but they're strangers and that might be rude

2024-05-19 20:04:31

- reply

It's been an interesting journey with this paper! We sent it to POPL last summer, where it got quite negative reviews, and we realized that the reviewers we got were not at all who we had been expecting. Our paper had been aimed squarely at Dependent Types Enjoyers. Instead, the reviewers were distributed systems verification experts. They weren't impressed by verification of logical clocks that everyone already knew were correct, and they didn't care about happens-before as a dependent type.

2024-05-19 19:26:58

- reply

Following up on this thread from October to share some good news: our work on causal separation diagrams is now published in PACMPL, and we'll present it at OOPSLA in October! 🎉 https://dl.acm.org/doi/10.1145/3649830
This project was led by @npub1x0e…f4mg, with a bit of help from @npub104w…d4l2 and me.

2023-10-06 19:51:06

- reply

I don't know the first thing about quantum computing. But I find the similarities striking. We have inductively defined diagrams that can be composed in sequence and in parallel; and so do they. Our "sites" seem to be analogous to their "wires", and our notion of happens-before seems related to their notion of connectivity. Not everything matches up perfectly, but a bunch of things do. Cool!

2023-10-06 19:47:39

- reply

Oh, one thing I forgot to add! Our work doesn't have to do with quantum computing -- or, at least, I didn't think it did -- but our formalism turns out to be uncannily similar to VyZX (https://arxiv.org/abs/2205.05781), a diagrammatic language for quantum computing, which I learned about from [@bhaktishh](https://types.pl/@bhaktishh ) at ICFP last month. The VyZX people wanted inductive diagrams to aid mechanized reasoning in a proof assistant, just like we did!

2023-10-05 06:03:47

- reply

❤️ Interpretability ❤️
We think that what makes our diagrams useful and interesting is their interpretability into various semantic domains: into types, into terms, into proofs relating types and terms. For the paper's case study on verified logical clocks, we wrote a series of interpreters for diagrams, culminating in an interpreter that *produces proofs about clocks*!
I'm really proud of this work, and there's lots more to do. We'll keep at it.

2023-10-05 05:55:46

- reply

🤯 A single, unified abstraction for processes and messages 🤯
The "sites" abstraction that our diagrams use generalizes over the notions of "process" and "message": a "site" is *any place where state exists*. Sending a message from a process is "forking" (or duplicating) a piece of that process’s state out into the world; receiving a message at a process is "joining" that message’s state with the process’s own. Conflating these two things is admittedly *weird*, but has some nice advantages!

2023-10-05 05:50:07

- reply

✨ Happens-before as a dependent type ✨
In Lamport’s traditional formulation of happens-before, the question “Does event A happen before event B?” just has a boolean answer: yes or no, and evidence of that answer exists separately. In our setting, you can't talk about a happens-before relationship without also talking about the causal path that witnesses the relationship. The answer to the question is either "no" or "yes, and here's why!"

2023-10-05 05:46:42

Now that it's been rejected from POPL, I can share what my students @npub1x0e…f4mg and @npub104w…d4l2 and I have been up to: a dependently-typed diagrammatic language for describing executions of concurrent systems! https://arxiv.org/abs/2307.10484
Here's what I think is cool about it. 👇