From Action Calculi to Linear Logic

9 years 4 months ago
From Action Calculi to Linear Logic
Abstract. Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm; the type theory has a sound and complete interpretation in Power’s categorical models. We go on to give a sound translation of our type theory in the (type theory of) intuitionistic linear logic, corresponding to the relation between Benton’s models of linear logic and models of action calculi. The conservativity of the syntactic translation is proved by a model-embedding construction using the Yoneda lemma. Finally, we briefly discuss how these techniques can also be used to give conservative translations between various extensions of action calculi.
Andrew Barber, Philippa Gardner, Masahito Hasegawa
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1997
Where CSL
Authors Andrew Barber, Philippa Gardner, Masahito Hasegawa, Gordon D. Plotkin
Comments (0)