Towards Effects in Mathematical Operational Semantics
| Autor: | Faris Abou-Saleh, Dirk Pattinson |
|---|---|
| Rok vydání: | 2011 |
| Předmět: |
Comodels
Effects General Computer Science Programming language Principle of compositionality Kleisli category Coalgebra computer.software_genre Monad (functional programming) Operational semantics Theoretical Computer Science Action semantics Denotational semantics Coalgebras TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Mathematics::Category Theory Computer Science::Logic in Computer Science Computer Science::Programming Languages Element (category theory) computer Computer Science(all) Mathematics |
| Zdroj: | MFPS |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2011.09.016 |
| Popis: | In this paper, we study extensions of mathematical operational semantics with algebraic effects. Our starting point is an effect-free coalgebraic operational semantics, given by a natural transformation of syntax over behaviour. The operational semantics of the extended language arises by distributing program syntax over effects, again inducing a coalgebraic operational semantics, but this time in the Kleisli category for the monad derived from the algebraic effects. The final coalgebra in this Kleisli category then serves as the denotational model. For it to exist, we ensure that the the Kleisli category is enriched over CPOs by considering the monad of possibly infinite terms, extended with a bottom element.Unlike the effectless setting, not all operational specifications give rise to adequate and compositional semantics. We give a proof of adequacy and compositionality provided the specifications can be described by evaluation-in-context. We illustrate our techniques with a simple extension of (stateless) while programs with global store, i.e. variable lookup. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect