Show simple item record

dc.contributor.authorBarber, Andrew G
dc.contributor.authorGardner, Phillipa
dc.contributor.authorHasegawa, Masahito
dc.contributor.authorPlotkin, Gordon
dc.coverage.spatial20en
dc.date.accessioned2003-11-06T10:21:07Z
dc.date.available2003-11-06T10:21:07Z
dc.date.issued1998
dc.identifier.citationCOMPUTER SCIENCE LOGIC LECTURE NOTES IN COMPUTER SCIENCE 1414: 78-97 1998en
dc.identifier.issn0302-9743
dc.identifier.urihttp://hdl.handle.net/1842/217
dc.description.abstractMilner 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.extent260176 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherSPRINGER-VERLAGen
dc.subjectLaboratory for Foundations of Computer Science
dc.titleFrom Action Calculi to Linear Logicen
dc.typePreprinten


Files in this item

This item appears in the following Collection(s)

Show simple item record