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.

• Type: Conference
• Year: 1997
• Where: CSL
• Authors: Andrew Barber, Philippa Gardner, Masahito Hasegawa, Gordon D. Plotkin
• Keywords: Action Calculi, Automated Reasoning, CSL 1997, Milner Introduced Action, Type Theory