### A dialectica model of state

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

#### Abstract

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$.