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
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.
[gzipped ps file]
[pdf file]
Pointers to Related Work
- A. Barber,
Linear Type Theories, Semantics and Action Calculi.
PhD thesis ECS-LFCS-97-371, University of Edinburgh (1997).
- N. Benton,
A mixed linear non-linear logic: proofs, terms and models.
In Proc. CSL'94, Springer LNCS 933 (1995) 121-135.
- P. Gardner and M. Hasegawa,
Types and models for higher-order action
calculi.
In Proc. TACS'97, Springer LNCS 1281 (1997) 583-603.
- R. Milner,
Calculi for interaction.
Acta Informatica 33(8) (1996) 707-737.
- A.J. Power,
Elementary control structures.
In Proc. CONCUR'96, Springer LNCS1119 (1996) 115-130.
Back to Hassei's
Research Page / Home Page