Edinburgh Research Archive

From Action Calculi to Linear Logic

Simple item page
dc.contributor.author
Barber, Andrew G
en
dc.contributor.author
Gardner, Phillipa
en
dc.contributor.author
Hasegawa, Masahito
en
dc.contributor.author
Plotkin, Gordon
en
dc.coverage.spatial
20
en
dc.date.accessioned
2003-11-06T10:21:07Z
dc.date.available
2003-11-06T10:21:07Z
dc.date.issued
1998
dc.description.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.
en
dc.format.extent
260176 bytes
en
dc.format.mimetype
application/pdf
en
dc.identifier.citation
COMPUTER SCIENCE LOGIC LECTURE NOTES IN COMPUTER SCIENCE 1414: 78-97 1998
dc.identifier.issn
0302-9743
dc.identifier.uri
http://hdl.handle.net/1842/217
dc.language.iso
en
dc.publisher
SPRINGER-VERLAG
en
dc.subject
Laboratory for Foundations of Computer Science
en
dc.title
From Action Calculi to Linear Logic
en
dc.type
Preprint
en

Files

Original bundle

Now showing 1 - 1 of 1
Name:
ActCalc_LinLog.pdf
Size:
254.08 KB
Format:
Adobe Portable Document Format
Download

This item appears in the following Collection(s)

Informatics Publications