You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
I posted this question in typ.zulipchat.com as well, but I thought I'd bring it here too because this server is much more active:
Is there research that uses separation logic to determine unrelated data flows that one could then turn around and use for vectorization? For instance, vectorized AES-XTS generates 8 or 16 tweaks ahead of time before it parallelizes the AES encrypt step—is there a way to generalize/formalize this type of optimization systematically? This implementation was done intuitively, but having a formal way of thinking about this could go a very long way!