M. da S. Corr\^ea
Departamento de Informatica,
Pontificia Univ. Catolica (PUC-Rio),
Rua Marques de Sao Vicente, 225,
Rio de Janeiro, RJ, 22453-900, Brazil.
correa@inf.puc-rio.br
E. H. Haeusler
Departamento de Informatica,
Pontificia Univ. Catolica (PUC-Rio),
Rua Marques de Sao Vicente, 225,
Rio de Janeiro, RJ, 22453-900, Brazil.
hermann@inf.puc-rio.br
V. C. V. de Paiva
Computer Laboratory,
University of Cambridge,
New Museums Site, Pembroke Street,
Cambridge CB2 3QG, U.K.
Valeria.Paiva@cl.cam.ac.uk
Reddy introduced an extended intuitionistic linear calculus, called LLMS (for Linear Logic Model of State), to model some features of state manipulation. His calculus includes the connective ``before'' and an associated modality $\dagger$. De Paiva presents a (collection of) dialectica categorical models for Classical Linear Logic, the categories GC. These categories contain an extra tensor product functor $\odot$ and a comonad structure corresponding to a modality related to this tensor. It is surprising that these works arising from completely different motivations can be related in a meaningful way. In this paper, we adapt Reddy's system LLMS providing it with a commutative version of the connective ``before'', denoted by $\odot$, and an associated modality. We show that such a new conective can be interpreted as the interleaving operator of CSP. We also construct a dialectica category G on Sets and show that it is a sound model for the modified system LLMS$_c$.