From action calculi to linear logic

Andrew Barber, Philippa Gardner, Masahito Hasegawa and Gordon Plotkin

In Annual Conference of the European Association for Computer Science Logic (CSL'97), Selected Papers, Springer LNCS 1414 (1998) 78-97


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.

[gzipped ps file]

[pdf file]

Pointers to Related Work

Back to Hassei's Research Page / Home Page