From Action Calculi to Linear Logic
View/ Open
Date
1998Author
Barber, Andrew G
Gardner, Phillipa
Hasegawa, Masahito
Plotkin, Gordon
Metadata
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.