=Paper=
{{Paper
|id=Vol-2046/steingartner-et-al
|storemode=property
|title=Some aspects about coalgebras as foundation for expressing the semantics of imperative languages
|pdfUrl=https://ceur-ws.org/Vol-2046/steingartner-et-al.pdf
|volume=Vol-2046
|authors=William Steingartner,Valerie Novitzká,Mohamed Ali M. Eldojali,Davorka Radaković
}}
==Some aspects about coalgebras as foundation for expressing the semantics of imperative languages==
https://ceur-ws.org/Vol-2046/steingartner-et-al.pdf
Some aspects about coalgebras as foundation for
expressing the semantics of imperative languages
William Steingartner1 , Valerie Novitzká1 ,
Mohamed Ali M. Eldojali1 , Davorka Radaković2
william.steingartner@tuke.sk, valerie.novitzka@tuke.sk,
eldojalimohamed@gmail.com, davorkar@dmi.uns.ac.rs
Technical University of Košice1 University of Novi Sad2
Faculty of Electrical Engineering and Informatics Faculty of Sciences
Košice, Slovakia Novi Sad, Serbia
Abstract
The semantics of programs written in some languages is concerned with
the interpretation in various types of models. Denotational seman-
tics expresses the meaning of programs by functions from syntactical
domains to semantic domains which can be non-trivial mathematical
structures. On the other hand, structural operational semantics de-
scribes the program behaviour in the form of states’ changes caused
by the execution of elementary steps. We present in this paper cate-
gorical representation of denotational semantics in category of states
as objects and semantic functions as morphisms. We present also cat-
egorical representation of structural operational semantics in category
as a transition system where states are objects and morphisms are ele-
mentary transitions. We also sketch how to define endofunctor on the
category of states and how to construct a Q-coalgebra of the functor.
1 Introduction
The semantics of programming languages belongs to the indisseverable parts of the definition of the languages.
Its role is to assign a meaning to a program written in a given programming language [Ded16]. There exist
several semantic methods varying in the way how to assign a meaning to a program text, e.g. denotational
semantics, natural semantics, operational semantics, axiomatic semantics, game semantics, action semantics and
others. These methods are equivalent mutually and we can choose such of them that is suitable for our purposes.
In this paper we deal with two semantic methods, denotational and operational semantics. Denotational
semantics expresses the meaning of a program in terms of domains and functions between them. Semantic
domains are mathematical structures, mainly lattices, and the meaning of a program is expressed as the elements
of them [Jas11]. The semantic functions map syntactic elements to the semantic domains and they are mainly
higher order functions. Denotational semantics was formulated by Dana Scott and Christopher Strachey [Sto77]
and later by David Schmidt [Sch97]. This method requires rather deep knowledge of mathematics; therefore it
is harder to perceive its principles for people that are not experienced in formal methods.
Copyright © by the paper’s authors. Copying permitted for private and academic purposes.
In: E. Vatai (ed.): Proceedings of the 11th Joint Conference on Mathematics and Computer Science, Eger, Hungary, 20th – 22nd of
May, 2016, published at http://ceur-ws.org
267
Operational semantics expresses each step of program execution in detail using transition relations. It provides
not only a meaning of a program but also its observable behaviour. This method requires medial knowledge
of mathematics and it is more understandable for practical programmers. Structural operational semantics was
formulated by Gordon Plotkin in [Plo81] and the main ideas and motivations are explained in [Plo04].
In the last decades the categorical structures have become useful for modeling the meanings of programs.
Categories are mathematical structures that consist of objects and morphisms between them. They enable to
work with more complex structures as the sets are and their properties can be represented also graphically. There
are several publications concerning with categorical denotational semantics, e.g. in [Ste15b]; they are based on a
category where the category objects, the semantic domains, represent the types of data structures and category
morphisms are operations. Such models are suitable primarily for functional programming languages.
When we are interested in behaviour of programs, operational semantics seems to be the most adequate
method. The useful categorical structures for operational semantics are coalgebras. They enable to generate
observable behaviour of a running program step by step [Plo04, Tur97]. A coalgebra can be considered as a
study of states and operations on them. The states form a state space that is hidden from an observer. A
relation between what is actually inside and what can be observed externally is the foundation of coalgebras
[Jac97]. Coalgebras are constructed using polynomial endofunctors over a category of states. In [Abo14] is
elaborated coalgebraic semantics for imperative languages with non-determinism and other effects. The author
constructs a monad over state space for the effects of a language and the behaviour of a program is obtained by
the composition of a polynomial endofunctor and a monad.
By contrast to the works in the area of denotational semantics and operational semantics mentioned above,
we attempt to define them so that they are both intelligible and demonstrative for students of computer science
and also for practical software engineers. The aim of our paper is to present principles of denotational and
operational semantics in terms of categories as simple as it is possible without loss of exactness. We define a
simple imperative language J ane with basic statements. In the case of denotational semantics we construct a
category of states, where the objects are states and morphisms are statements. For operational semantics we
construct also a category of states where the objects are states but morphisms are transition functions. We model
behaviour of programs as an appropriate endofunctor over this category as a coalgebra. In the both cases we use
the categories which objects are sets and we discuss the properties of them to be legal categories. The advantage
of our approach is that it provides precise graphically illustrated denotational and operational semantics without
need of deeper knowledge of mathematics and therefore it is suitable for teaching.
The effectiveness of categories is in their expressive power. Categorical models are highly illustrative and
their graphical representations are very good readable and understandable. The effectiveness of coalgebras we
showed in [Ste16] where we presented construction of coalgebra for concrete programming problem taught on
SLGeometry tool. Then the next step could be a construction of an appropriate transition system as category
of states. Moreover, categorical semantic methods are suitable also for e-Learning education process. They can
be easily implemented and integrated into standard e-Learning tools such as LMS Moodle.
2 Language J ane
In our paper we use a simple language J ane. This language consists of traditional syntactic constructions
of imperative languages, namely arithmetic and Boolean expressions and statements. For this language the
well-known syntactic domains are introduced:
n ∈ Num - digit strings
x ∈ Var - variable names
e ∈ Aexpr - arithmetic expressions
b ∈ Bexpr - Boolean expressions
S ∈ Statm - statements
Five Dijkstra’s elementary statements that are elements of the syntactic domain Statm, S ∈ Statm, are
considered: assignment, empty statement, sequence of statements, conditional statement and cycle statement:
S ∶∶= x ∶= e ∣ skip ∣ S; S ∣ if b then S else S ∣ while b do S.
The semantics of arithmetic and Boolean expressions was formulated in [Ste15a]. For preservation of simplicity,
here we do not consider blocks, input statement and declarations.
268
3 The states as memory abstraction
A program in J ane is a sequence of the statements. Execution of a program causes a change of some memory
cells. Every snapshot of a memory during program execution can be abstracted as a state where program
variables have assigned some values. Execution of a statement can modify some values of program variables, i.e.
a state is changed. A meaning of a program is then the change of an initial state before program execution to
a final state after program execution. Therefore state is a basic concept in the definition of formal semantics of
imperative languages.
We define the semantic domain State as an abstract data type with the following signature:
ΣState =
types ∶ State, V ar, V alue
opns ∶ init ∶→ State
get ∶ V ar, State → V alue
V ar and V alue are type names for program variables and values, respectively. The operation specifications have
the following intuitive meaning:
• init merely creates the initial state of a program;
• get returns a variable value in a given state.
Now we assign the representation to the signature of states ΣState . We assign to the type V alue the set of
integer numbers together with the undefined value :
Value = Z ∪ {} . (1)
We assign to the type V ar a countable set Var of variable names. Our representation of an element of type
State has to express a variable name and its value.
We assign to the type State the set State of states. Every state s ∈ State is represented as a function
s ∶ Var → Value. (2)
Each state s expresses one moment of program execution. We express a state s as a sequence:
s = ⟨(x, v1 ) , . . . , (z, vn )⟩
of ordered tuples
(x, v) ,
where x is the name of a variable with its actual value v.
We define representations of operation specifications from the signature ΣState as follows. The operation JinitK
defined by
JinitK = s0 , (3)
creates the initial state s0 of a program possibly with input values of variables. Its role is to create a new
sequence of state at the beginning of program execution.
The operation JgetK returns the value of a variable and is defined by
JgetK(x, ⟨. . . , (x, vi ), . . . , (z, vk ), . . .⟩) = vi , (4)
from the definition of state.
States defined above will be category objects in our model. We also consider a special state
s = ⟨(, )⟩ (5)
expressing the undefined state.
269
Jx := eK
s s0
Figure 1: Execution of assignment statement
JskipK
s
Figure 2: Execution of empty statement
4 Categorical denotational semantics of J ane
Now we construct a model of language J ane as a category of states, CState . In this category we consider:
• states as category objects; and
• semantic functions as category morphisms.
Statements execute program actions, i.e. they get values from the actual state and possibly provide new values.
A state is changed if a value of a program variable is modified. We model the change of states as the semantic
function JSK between states, where S is a statement:
JSK ∶ s → s′ , (6)
where s and s are states. This function is partially defined, because the resulting state s can be undefined. To
′ ′
be a semantic function a morphism in CState , we extend JSK to total function using a special object of undefined
state s :
JSK ∶ s → s (7)
if a statement S has undefined meaning in its input state s.
Category CState has to satisfy the following axioms from the definition of categories [Bar90]:
• each object has identity morphism;
• for two composable morphisms there exists a morphism that is their composition.
A morphism is CState is an application of the semantic function JSK. As we see bellow, the role of identity
morphism plays the semantic function applied on the empty statement. The second axiom is satisfied in the case
of sequence of statements. Therefore we can state that CState is a category.
We follow with the definition of the semantic function JSK for J ane statements. Assignment statement x ∶= e
assigns a value of an arithmetic expression e in a state s to the variable x.
The semantic function for assignment statement is defined as follows:
s [(x, v) ↦ (x, JeKs)] , for (x, v) ∈ s;
Jx ∶= eKs = { (8)
s , otherwise
and it is illustrated in Figure 1.
The empty statement skip does not do anything, i.e. it does not change the state. Clearly, the semantic
function applied on the empty statement is the identity morphism on a state s (Figure 2) and it is defined by:
JskipKs = s. (9)
A sequence of statements S1 ; S2 is executed one by one and can be modeled as a composition of morphisms
(Figure 3)
JS1 ; S2 K = JS2 K ○ JS1 K (10)
270
JS1; S2K
JS1K
s
s0
s00
JS2K
Figure 3: Composition of functions for statement sequence
s s0
Figure 4: Execution of conditional statement
defined for a state s by
JS1 ; S2 Ks = JS2 K (JS1 K) s. (11)
If a state s′ is undefined, i.e. s′ = s , then the execution of the whole sequence of statements provides undefined
state:
JSKs = s . (12)
From this definition follows that achieving undefined state s is similar as falling into ”black hole”. It means
that execution of a program is immediately stopped without resulting state. Because a program in J ane is a
sequence of statements, we can state that a meaning of a program is either a path (morphism composition) from
the initial state s0 to a final state s or it is undefined when the path ends in the undefined state s .
Conditional statement
if b then S1 else S2
causes branching of execution depending on the value of a Boolean expression. The semantic function for
conditional statement is defined as:
⎧
⎪ JS1 Ks, if JbKs = true;
⎪
⎪
Jif b then S1 else S2 Ks = ⎨ JS2 Ks, if JbKs = false; (13)
⎪
⎪
⎪
⎩ s , otherwise.
It is interesting that the path of a program can follow either to the state JS1 Ks or to the state JS2 Ks, i.e.
deterministically and the branching is unseen in CState as it is illustrated in Figure 4. The result state s′ can be
either JS1 Ks or JS2 Ks, but only one of them.
Now we consider cycle statement
while b do S
Its execution also depends on the value of Boolean expression b. If JbKs evaluates to true in an actual state s,
the body S of a cycle is executed, then again b is evaluated in a possibly modified state. If JbKs evaluates to
false, execution of cycle statement is finished and we obtain the result state.
The traditional denotational semantics of a cycle statement is defined by using fixpoint operator. This
approach is obvious if the categorical model is a category of types. Existence of the least fixed point ensures
that while statement finishes, in the other case the execution of while statement is infinite, i.e. the denotational
semantics of this statement is not defined. This approach is discussed in detail in [Nie07, Sch97]. In general,
the computational categorical models have continuous lattices as objects and continuous functions as morphisms
[Sto77]. Such models require some structure on endomorphisms [Esc07].
In our approach we use categorical model with states as objects and functions as morphisms. The domains
(states) are sets, not lattices; therefore we use another concept for handling infinite cycles. The execution of
a while statement is a path of morphisms, i.e. a composition of morphisms. This path can be either finite or
271
infinite and we need some construction in our category to solve both cases. The useful construct is the colimit
of a diagram. Consider a diagram D consisting of the composition of morphisms
D ∶ s0 → s1 → s2 → . . . si → si+1 → . . . (14)
This composition of morphisms is a composition of semantic functions applied on while statement with actual
states. This infinite composition is a morphism
s0 → s∞
for which there are morphisms fi∞ ∶ si → s∞ for i ≥ 0 such that the cocone in Figure 5 is a colimit of the diagram
D.
s∞
∞
fi+1
fi∞
f0∞ f1∞ f2∞
s0 s1 s2 . . . si si+1 . . .
Figure 5: Colimit of infinite composition of states
Then we can define the semantic function for while statement as:
s′ , if D is finite
Jwhile b do SKs = { (15)
colim(D), if D is infinite
Because the objects in CState are sets, such colimits always exist.
5 Example of categorical denotational semantics
We present in this section a short example. We show how to find a semantics of program, that calculates integer
division and modulo. Let the program S0 be the following:
z ∶= 0;
while (y ≤ x) do (z ∶= z + 1; x ∶= x − y);
and let the input state be s0 = [x ↦ 17, y ↦ 5]. We assume in variable x a divident, and in variable y a divisor.
We introduce the following substitutions in our program:
S1 = z ∶= 0
S2 = while (y ≤ x) do (z ∶= z + 1; x ∶= x − y)
A meaning of the program S in an input state s0 is given as follows:
JS1 ; S2 Ks0 = JS2 K (JS1 Ks0 ) = JS2 Ks1 = JS2 K (Jx ∶= x − yK (Jz ∶= z + 1Ks1 ))
= JS2 K (Jx ∶= x − yKs2 ) = JS2 Ks3 = JS2 K (Jx ∶= x − yK (Jz ∶= z + 1Ks3 ))
= JS2 K (Jx ∶= x − yKs4 ) = JS2 Ks5 = JS2 K (Jx ∶= x − yK (Jz ∶= z + 1Ks5 ))
= JS2 K (Jx ∶= x − yKs6 ) = JS2 Ks7 = id(s7 ) = s7
Particular states during the program execution are listed in Figure 6.
Expected results are: a quotient is after the execution stored in the variable z and remainder in variable x.
We can observe that program is expressed as a compound function consisting of more morphisms which form
together a path in category. The compound function is constructed as follows:
JSK = JskipK ○ Jx ∶= x − yK ○ Jz ∶= z + 1K ○ Jx ∶= x − yK ○ Jz ∶= z + 1K ○ Jx ∶= x − yK ○ Jz ∶= z + 1K ○ Jz ∶= 0K. (16)
272
s0 s1 s2 s3
x 17 x 17 x 17 x 12
y 5 y 5 y 5 y 5
z ε z 0 z 1 z 1
s4 s5 s6 s7
x 12 x 7 x 7 x 2
y 5 y 5 y 5 y 5
z 2 z 2 z 3 z 3
Figure 6: States during the program S execution
CState
s2
s3
s0
s7
s1 s4
s6
s5
Figure 7: Path in category of states
An illustration of a path in category CState representing a compound morphism for a semantics of the whole
program S is depicted in Figure 7.
A categorical operational semantics of this program is in Section 7.
◻
6 Categorical operational semantics as transition system
We defined categorical semantics of language J ane in the previous section based on denotational approach.
In this section we shortly describe how to construct a categorical model based on operational semantics. Its
main features are detailed description of program execution in small steps and following observable behaviour
of a program. The execution of a program can be expressed also graphically which is highly illustrative and it
accentuates the dynamics of structural operational semantics.
A model of structural operational semantics is a transition system which models program behaviour on a state
space [Jon03, Plo04]. The change of state is defined for particular statements by inference rules.
A transition
⟨S, s⟩ ⇒ s′
is a relation between input state s and output state s′ . A change of state is done as one-step action [Rad13]. If
a statement is not being executed in one step, then a transition can be written as:
⟨S, s⟩ ⇒ ⟨S ′ , s′ ⟩ .
273
In both cases a transition rule expresses one action during the program execution. The inference rules for J ane
in structural operational semantics are the following [Nie07]:
⟨x ∶= e, s⟩ ⇒ s[x ↦ JeKs] (1os )
⟨skip, s⟩ ⇒ s (2os )
⟨S1 , s⟩ ⇒ ⟨S1′ , s′ ⟩ ⟨S1 , s⟩ ⇒ s′
(31 ) (32 )
⟨S1 ; S2 , s⟩ ⇒ ⟨S1′ ; S2 , s′ ⟩ os ⟨S1 ; S2 , s⟩ ⇒ ⟨S2 , s′ ⟩ os
JbKs = true JbKs = false
(4true ) (4false )
⟨if b then S1 else S2 , s⟩ ⇒ ⟨S1 , s⟩ os ⟨if b then S1 else S2 , s⟩ ⇒ ⟨S2 , s⟩ os
The inference rule for prefix cycle uses semantic equivalence:
⟨while b do S, s⟩ ⇒ ⟨if b then (S; while b do S) else skip, s⟩ (5os )
In these inference rules, JeK and JbK are semantic functions, which assign to any syntactic well-formed expressions
their meanings - an integer value, a Boolean value, resp. The result of the functions JeK and JbK, where e stands
for an arithmetic expression and b stands for a Boolean expression, depend on an actual state
JeK ∶ State → Value,
JbK ∶ State → {false, true} .
Function produces transient data, that are consumed during the program execution and their values are never
stored into memory - they are used only for affecting the control flow in a program.
A categorical structure that models observable behaviour of programs is a coalgebra. It is constructed over a
base category of states using a polynomial endofunctor. A base category DState consists of
• objects that are states from State; and
• morphisms that are transitions.
The objects of DState are the same as for the category CState constructed for categorical denotational semantics
but these two categories differ in morphisms. Because we need transitions as morphisms, we define the transition
function next:
next ∶ Statm → (State → State),
that return for a statement S
nextJSK ∶ State → State
the next state obtained from the execution of the first step of a statement JSK. We define this function for
statements in J ane by:
⎧
⎪ s′ = s [x ↦ JeK] if S = x ∶= e;
⎪
⎪
⎪
⎪
⎪
⎪ s if S = skip
⎪
⎪
⎪ or S = while b do S and JbKs = false;
⎪
⎪
⎪
⎪
⎪
⎪ nextJS1′ ; S2 K(s′ ) if S = S1 ; S2 and ⟨S1 ; S2 , s⟩ ⇒ ⟨S1′ ; S2 , s′ ⟩ ;
⎪
nextJSK(s) = ⎨ nextJS2 K(s′ ) if S = S1 ; S2 and ⟨S1 ; S2 , s⟩ ⇒ ⟨S2 , s′ ⟩ ; (17)
⎪
⎪
⎪
⎪
⎪ nextJS1 K(s) if S = if b then S1 else S2 and JbKs = true;
⎪
⎪
⎪
⎪
⎪ nextJS2 K(s) if S = if b then S1 else S2 and JbKs = false;
⎪
⎪
⎪ nextJS; while b do SK(s) if S = while b do S and JbKs = true;
⎪
⎪
⎪
⎪
⎩ abort(s) otherwise.
From this definition follows that any morphism in the category of states DState can be considered as an application
of function nextJSK for a given statement.
Now we construct the polynomial endofunctor
Q ∶ DState → DState
274
that to any statement S and an object s assigns the next state or undefined state. The name polynomial [Koc12]
indicates the polynomial form of a functor constructed using products and coproducts. For our purposes we
define a functor
Q(State) = 1 + State
where State is a state space. We define this functor for objects and morphisms in DState as follows:
Q(s) = s + nextJSKs
Q(nextJSK) = abort + nextJSK
where abort is a unique morphism which sends any state to the undefined state s :
abort ∶ s ⇢ s (18)
and it represents the situation when an error occurs during the program execution and the program cannot
continue its execution. Because from any object in a category there exists only one morphism into the undefined
state, it is an object which has a property of terminal object 1 in the category.
A Q-coalgebra, also called coalgebra of type Q or Q-system, is a pair (State, nextJSK), where State is a state
space of the coalgebra and nextJSK is the structure map of the coalgebra on State:
nextJSK ∶ State → Q(State).
This structure map acts as a destructor. It takes an element of the Q-coalgebra and decomposes the element
into its constituent parts. This is a common feature of coalgebras and this point of view is dual to the point of
view that algebras are objects together with combinatory principles [Hug01].
7 Example of categorical operational semantics
We present in this section a short example of finding a meaning of a program in categorical operational semantics.
We continue with the same program as in Section 5 - we show how to find a semantics of program, that calculates
integer division and modulo. The code of program S0 is:
z ∶= 0;
while (y ≤ x) do (z ∶= z + 1; x ∶= x − y);
and let the input state be again s0 = [x ↦ 17, y ↦ 5]. We assume in variable x a divident, and in variable y a
divisor. We follow the substitutions in our program from Section 5:
S1 = z ∶= 0
S2 = while (y ≤ x) do (z ∶= z + 1; x ∶= x − y)
Here the coalgebra state space is the set of category objects Ob(CState ) = State and 1 = {s } is a singleton
set containing only an undefined state. The endofunctor on category of states is defined as follows:
Q(State) = 1 + State,
and it sends objects s ∈ State to objects:
Q(s) = s + nextJSKs,
and morphisms to morphisms:
Q(nextJSK) = abort + nextJSK
275
Now we construct the sequence of states:
Q(s0 ) = 1 + nextJS0 Ks0 = nextJS1 ; S2 Ks0
= nextJS2 Ks1
= nextJz ∶= z + 1; x ∶= x − y; S2 Ks1
= nextJx ∶= x − y; S2 Ks2
= nextJS2 Ks3
= nextJz ∶= z + 1; x ∶= x − y; S2 Ks3
= nextJx ∶= x − y; S2 Ks4
= nextJS2 Ks5
= nextJz ∶= z + 1; x ∶= x − y; S2 Ks5
= nextJx ∶= x − y; S2 Ks6
= nextJS2 Ks7
= s7
Particular states and evaluation of Boolean condition during the program execution are as follows:
s0 = ⟨(x, 17), (y, 5)⟩
s1 = ⟨(x, 17), (y, 5), (z, 0)⟩ Jy ≤ xKs1 = true
s2 = ⟨(x, 17), (y, 5), (z, 1)⟩
s3 = ⟨(x, 12), (y, 5), (z, 1)⟩ Jy ≤ xKs3 = true
s4 = ⟨(x, 12), (y, 5), (z, 2)⟩
s5 = ⟨(x, 7), (y, 5), (z, 2)⟩ Jy ≤ xKs5 = true
s6 = ⟨(x, 7), (y, 5), (z, 3)⟩
s7 = ⟨(x, 2), (y, 5), (z, 3)⟩ Jy ≤ xKs7 = false
Expected results are: a quotient is after the execution stored in the variable z and remainder in the variable x.
◻
8 Conclusion
We presented in our paper a new approach how to define denotational semantics and operational one in terms
of categories. In both cases a state is a basic concept. A state represents a snapshot of a memory that can be
changed during the program execution. In denotational approach category objects are states and morphisms are
functions on states. We discussed also how to solve the situation of infinite sequence of states using colimits of
diagrams. In the operational semantics the category objects are also states but the morphisms are transitions,
i.e. elementary actions representing detailed steps of execution. The behaviour of a program is obtained by
polynomial endofunctor and structure map of coalgebra.
Very high illustrative power of categories is very fruitful for innovative didactic methods used in education
process of young software engineers and IT experts.
We want to extend our approach by introducing and modeling also user inputs and outputs, blocks, variable
declarations and procedures and then to construct denotational and operational semantics for real programming
language in categorical terms by following our ideas in [Ste17].
Acknowledgements
This work has been supported by Grant No. 002TUKE-4/2017: Innovative didactic methods of education process
at university and their importance in increasing education mastership of teachers and development of students
competences.
References
[Abo14] Abou-Saleh, F.: A coalgebraic semantics for imperative programming languages. Imperial College
London, UK 2014.
[Ada06] Adámek, J., Herrlich, H., Strecker, G.: Abstract and concrete categories: The joy of cats. Reprints in
Theory and Applications of Categories, No. 17, 2006.
276
[Bar90] Barr, M., Wells, C.: Category theory for computing science, Prentice-Hall, Inc., Upper Saddle River,
NJ, USA, 1990.
[Ded16] Dedera L., Benčı́k M.: Language representations based on C-BML and their processing (2016). Ad-
vances in Military Technology, Vol. 11, No. 2, pp. 159-170.
[Esc07] Escardó, M.H.: Recursion and Induction on the Real Line, In: Proceedings for the Second Imperial Col-
lege Department of Computing Workshop on Theory and Formal Methods, Møller Centre, Cambridge,
11-14 September 1994.
[Hug01] Hughes J.: A Study of Categories of Algebras and Coalgebras, Ph.D. thesis, Carnegie Mellon University,
Pittsburgh PA, USA, 2001.
[Jac97] Jacobs, B., Rutten, J.: A Tutorial on (Co)Algebras and (Co)Induction, EATCS Bulletin Vol. 62, 1997,
pp. 222-259.
[Jac05] Jacobs, B.: Introduction to coalgebra. Towards Mathematics of States and Observations (draft) (2005).
[Jas11] Jaskelioff, M., Ghani, N., Hutton, G.: Modularity and Implementation of Mathematical Operational
Semantics, Electronic Notes in Theoretical Computer Science, Vol. 229, No. 5, 2011, pp. 75–95, Pro-
ceedings of the Second Workshop on Mathematically Structured Functional Programming, MSFP 2008.
[Jay91] Jay, B.: Fixpoint And Loop Constructions As Colimits, Lecture Notes In Mathematics, Vol. 1488, pp.
187-192, 1991.
[Jon03] Jones, C. B.: Operational Semantics: Concepts and Their Expression, Information Processing Letters,
Vol. 88, No. 1-2, 2003, pp. 27–32.
[Koc12] Kock, J.: Data types with symmetries and polynomial functors over groupoids. In Proceedings of the
28th Conference on the Mathematical Foundations of Programming Semantics, Bath 2012, Electronic
Notes in Theoretical Computer Science, Vol. 286, 2012, pp. 351–365.
[Kur01] Kurz, A.: Coalgebras and Modal Logic. Course Notes for ESSLLI 2001, Version of October 2001.
Appeared on the CD-Rom ESSLLI’01, Department of Philosophy, University of Helsinki, Finland.
[Nie07] Riis Nielson, H., Nielson, F.: Semantics With Applications: An Appetizer, Springer-Verlag London,
2007.
[Nov08] Novitzká, V., Mihályi, D., and Verbová, A.: Coalgebras as models of systems behaviour. In Interna-
tional Conference on Applied Electrical Engineering and Informatics, Greece, Athens (2008), pp. 31–36.
[Per15] Perháč, J., Mihályi, D.: Intrusion Detection System Behavior as Resource-Oriented Formula, Acta
Electrotechnica et Informatica, Vol. 15, No. 3, Technical University of Košice, Slovakia, 2015.
[Plo81] Plotkin, G. D.: A Structural Approach to Operational Semantics, Technical Report DAIMI FN-19,
University of Aarhus, 1981.
[Plo04] Plotkin, G. D.: The Origins of Structural Operational Semantics, J. Log. Algebr. Program., Vol. 60-61,
2004, pp. 3–15.
[Rad13] Radaković, D., Herceg, D.: A Platform for Development of Mathematical Games on Silverlight, Acta
Didactica Napocensia, Vol. 6, No. 1, Babeş-Bolyai University, pp. 77-90, 2013.
[Sch97] Schmidt, D.: Denotational Semantics. A methodology for language development, 1997.
[Slo11] Slodičák, V., Macko, P.: Some New Approaches in Functional Programming Using Algebras and Coal-
gebras, Electronic Notes on Theoretical Computer Science, Vol. 279, No. 3, 2011, pp. 41–62.
[Ste15a] Steingartner, W., Novitzká, V.: A new approach to operational semantics by categories, Proceedings of
the 26th Central European Conference on Information and Intelligent Systems, CECIIS 2015, Varaždin,
University of Zagreb, 2015.
277
[Ste15b] Steingartner, W., Novitzká, V.: A new approach to semantics of procedures in categorical terms,
Proceedings of 2015 IEEE 13th International Conference Informatics, Poprad, Slovakia, IEEE Danvers,
2015, pp. 252–257.
[Ste16] Steingartner, W., Radaković, D., Valkošák, F., Macko, P.: Some properties of coalgebras and their rôle
in computer science, Journal of Applied Mathematics and Computational Mechanics, Vol. 15, No. 4,
2016, pp. 145-156.
[Ste17] Steingartner, W., Radaković, D., Novitzká, V., Eldojali, M. A.: An Analysis of Some Aspects of
Component-Based Programming for Selecting Appropriate Categorical Structures as their Models, Acta
Electrotechnica et Informatica, Vol. 17, No. 2, Technical University of Košice, Slovakia, 2017.
[Sto77] Stoy, J. E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory,
MIT Press, Cambridge, MA, USA, 1977.
[Tay93] Taylor, P.: An Exact Interpretation of While. In: Theory and Formal Methods 1993: Proceedings of
the First Imperial College Department of Computing Workshop on Theory and Formal Methods, Isle
of Thorns Conference Centre, Chelwood Gate, Sussex, UK, 29–31 March 1993, Springer London, pp.
302–313, 1993.
[Tur97] Turi, D., Plotkin, G.: Towards a Mathematical Operational Semantics, In Proc. 12 th LICS Conf.,
IEEE, Computer Society Press, 1997.
278