Towards a non-commutative logic of effects

I will present work-in-progress (with Jonas Frey and Paul-André Melliès) aimed at establishing closer links between the theory of
computational effects and linear logic in the broad sense. Starting from an analogy between polarity and "Isbell duality", I will describe
a new categorical interpretation of (polarized, non-commutative) linear logic, and suggest its potential applications for describing
and reasoning about programs with side effects. In particular, I will consider as a case study Reynolds' equation "intvar = intexp &
intacc", defining an integer variable (in the Forsythe language) as the intersection of an integer expression and an integer acceptor.