Tensors of comodels and models for operational semantics

G Plotkin; John Power

doi:10.1016/j.entcs.2008.10.018

Tensors of comodels and models for operational semantics

G Plotkin, John Power

Department of Computer Science

Research output: Contribution to journal › Article › peer-review

19 Citations (SciVal)

132 Downloads (Pure)

Abstract

In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C, typically the final one, and a model M, typically free; one then seeks a previous termtensornext termC⊗M of the comodel with the model that allows operations to flow between the two. We describe such a previous termtensornext term implicit in the abstract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state.

Original language	English
Pages (from-to)	295-311
Number of pages	17
Journal	Electronic Notes in Theoretical Computer Science
Volume	218
DOIs	https://doi.org/10.1016/j.entcs.2008.10.018
Publication status	Published - 22 Oct 2008

Access to Document

10.1016/j.entcs.2008.10.018

Power_ENTCS_2008_218_295.pdf
NOTICE: this is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Electronic Notes in Theoretical Computer Science, Vol 218, 2008, DOI 10.1016/j.entcs.2008.10.018
Accepted author manuscript, 1.2 MB

Cite this

@article{ea8e570b10d242b4a8444c7d9d816622,

title = "Tensors of comodels and models for operational semantics",

abstract = "In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C, typically the final one, and a model M, typically free; one then seeks a previous termtensornext termC⊗M of the comodel with the model that allows operations to flow between the two. We describe such a previous termtensornext term implicit in the abstract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state.",

author = "G Plotkin and John Power",

note = "Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV)",

year = "2008",

month = oct,

day = "22",

doi = "10.1016/j.entcs.2008.10.018",

language = "English",

volume = "218",

pages = "295--311",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - Tensors of comodels and models for operational semantics

AU - Plotkin, G

AU - Power, John

N1 - Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV)

PY - 2008/10/22

Y1 - 2008/10/22

N2 - In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C, typically the final one, and a model M, typically free; one then seeks a previous termtensornext termC⊗M of the comodel with the model that allows operations to flow between the two. We describe such a previous termtensornext term implicit in the abstract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state.

AB - In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C, typically the final one, and a model M, typically free; one then seeks a previous termtensornext termC⊗M of the comodel with the model that allows operations to flow between the two. We describe such a previous termtensornext term implicit in the abstract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state.

UR - http://www.scopus.com/inward/record.url?scp=54049145172&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1016/j.entcs.2008.10.018

U2 - 10.1016/j.entcs.2008.10.018

DO - 10.1016/j.entcs.2008.10.018

M3 - Article

SN - 1571-0661

VL - 218

SP - 295

EP - 311

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Tensors of comodels and models for operational semantics

Abstract

Access to Document

Other files and links

Fingerprint

Cite this