Category Theory
Zulip Server
Archive

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.


Stream: practice: software

Topic: Separation Logic and Vectorization


view this post on Zulip dan pittman (Mar 04 2025 at 00:40):

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!