GitLab

It seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. We could remove implication from the MoSeL interface and see what happens.

For Iris itself I mostly expect this to work, but the general linear case might make this harder. Or not.