Comodels and effects in mathematical operational semantics

Faris Abou-Saleh; Dirk Pattinson

doi:10.1007/978-3-642-37075-5_9

Comodels and effects in mathematical operational semantics

Faris Abou-Saleh^*, Dirk Pattinson

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

5 Citations (Scopus)

Abstract

In the mid-nineties, Turi and Plotkin gave an elegant categorical treatment of denotational and operational semantics for process algebra-like languages, proving compositionality and adequacy by defining operational semantics as a distributive law of syntax over behaviour. However, its applications to stateful or effectful languages, incorporating (co)models of a countable Lawvere theory, have been elusive so far. We make some progress towards a coalgebraic treatment of such languages, proposing a congruence format related to the evaluation-in-context paradigm. We formalise the denotational semantics in suitable Kleisli categories, and prove adequacy and compositionality of the semantic theory under this congruence format.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.
Pages	129-144
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-37075-5_9
Publication status	Published - 2013
Event	16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013 - Rome, Italy Duration: 16 Mar 2013 → 24 Mar 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7794 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
Country/Territory	Italy
City	Rome
Period	16/03/13 → 24/03/13

Access to Document

10.1007/978-3-642-37075-5_9

Cite this

Abou-Saleh, F., & Pattinson, D. (2013). Comodels and effects in mathematical operational semantics. In Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc. (pp. 129-144). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7794 LNCS). https://doi.org/10.1007/978-3-642-37075-5_9

Abou-Saleh, Faris ; Pattinson, Dirk. / Comodels and effects in mathematical operational semantics. Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. 2013. pp. 129-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{bc453dc435bc487fa706fbc8b316bbbf,

title = "Comodels and effects in mathematical operational semantics",

abstract = "In the mid-nineties, Turi and Plotkin gave an elegant categorical treatment of denotational and operational semantics for process algebra-like languages, proving compositionality and adequacy by defining operational semantics as a distributive law of syntax over behaviour. However, its applications to stateful or effectful languages, incorporating (co)models of a countable Lawvere theory, have been elusive so far. We make some progress towards a coalgebraic treatment of such languages, proposing a congruence format related to the evaluation-in-context paradigm. We formalise the denotational semantics in suitable Kleisli categories, and prove adequacy and compositionality of the semantic theory under this congruence format.",

author = "Faris Abou-Saleh and Dirk Pattinson",

year = "2013",

doi = "10.1007/978-3-642-37075-5_9",

language = "English",

isbn = "9783642370748",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "129--144",

booktitle = "Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.",

note = "16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013 ; Conference date: 16-03-2013 Through 24-03-2013",

}

Abou-Saleh, F & Pattinson, D 2013, Comodels and effects in mathematical operational semantics. in Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7794 LNCS, pp. 129-144, 16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, 16/03/13. https://doi.org/10.1007/978-3-642-37075-5_9

Comodels and effects in mathematical operational semantics. / Abou-Saleh, Faris; Pattinson, Dirk.
Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. 2013. p. 129-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7794 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Comodels and effects in mathematical operational semantics

AU - Abou-Saleh, Faris

AU - Pattinson, Dirk

PY - 2013

Y1 - 2013

N2 - In the mid-nineties, Turi and Plotkin gave an elegant categorical treatment of denotational and operational semantics for process algebra-like languages, proving compositionality and adequacy by defining operational semantics as a distributive law of syntax over behaviour. However, its applications to stateful or effectful languages, incorporating (co)models of a countable Lawvere theory, have been elusive so far. We make some progress towards a coalgebraic treatment of such languages, proposing a congruence format related to the evaluation-in-context paradigm. We formalise the denotational semantics in suitable Kleisli categories, and prove adequacy and compositionality of the semantic theory under this congruence format.

AB - In the mid-nineties, Turi and Plotkin gave an elegant categorical treatment of denotational and operational semantics for process algebra-like languages, proving compositionality and adequacy by defining operational semantics as a distributive law of syntax over behaviour. However, its applications to stateful or effectful languages, incorporating (co)models of a countable Lawvere theory, have been elusive so far. We make some progress towards a coalgebraic treatment of such languages, proposing a congruence format related to the evaluation-in-context paradigm. We formalise the denotational semantics in suitable Kleisli categories, and prove adequacy and compositionality of the semantic theory under this congruence format.

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

U2 - 10.1007/978-3-642-37075-5_9

DO - 10.1007/978-3-642-37075-5_9

M3 - Conference contribution

SN - 9783642370748

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 129

EP - 144

BT - Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.

T2 - 16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013

Y2 - 16 March 2013 through 24 March 2013

ER -

Abou-Saleh F, Pattinson D. Comodels and effects in mathematical operational semantics. In Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. 2013. p. 129-144. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-37075-5_9

Comodels and effects in mathematical operational semantics

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this