Help understand the notation

I'm reading a computer science paper, this one: https://arxiv.org/abs/1608.03960. It uses certain notation in one of the illustrations (Figure 9, page 8 in the PDF version) that I don't understand how to interpret.
Attaching here as well for better visibility:

$$ \text{EXEC} ~ \frac{\text{cmd}_1 : \text{CMD} \quad A_p, \text{cmd}_1 \implies A^\prime_p}{A_p, \langle \text{cmd}_1 ~ ; ~ \text{cmd}_2 ~ ; \ldots \rangle \implies A^\prime_p, \langle \text{cmd}_2 ~ ; \ldots \rangle} $$

I've tried to search for this online, but haven't come up with anything. I'd appreciate if someone explain it to me, particularly these questions:

-
Does this notation has an official or widely recognized name?

-
What's the relationships between expression above and below the horizontal line?

-
What's the meaning of $\Rightarrow$, long arrow?

-
What's the meaning of two expressions being separated by a comma, as in $A_p, cmd_1$? How is it different from two expressions separated by a blank space, as in $$\mathrm{cmd}_1, \mathrm{CMD}\ \ \ \ \ \ \ \ A_p, \mathrm{cmd}_1\,?$$

Here's another example from the paper:

$$ \text{VAR} ~\frac{x \in \text{dom}(A_p)}{A_p, x \implies A_p(x)}$$

• What's the meaning of $dom(A_p)$ here?

Answering your questions one by one:

• The rules are part of an operational semantics, which defines how to evaluate expressions.

• The notation with the horizontal line is an inference rule: if all the logical statements above the line are true, then you can conclude that the statement below the line is also true.

• The arrow is a predicate that indicates that the left hand side can be evaluated (or reduced) to the right hand side.

• The expressions separated by a comma form a tuple; for example, $A_p, cmd_1$ is a pair consisting of $A_p$ and $cmd_1$.

• $\mathrm{dom}(f)$ returns the domain of the function $f$, that is, the set of values $x$ for which $f(x)$ is defined.

In these rules, $A_p$ is a state object: a function that maps variable names to values. (Think of it a bit like the heap on which you can allocate objects, and where the variable names are pointers.) The VAR rule performs variable lookup in that state:

• If the statement above the line is true: $x \in \mathrm{dom}(A_p)$, that is, the function $A_p$ is defined for the argument $A_p(x)$,

• Then the statement below the line is true: $A_p, x \Longrightarrow A_p(x)$, that is, the expression $x$ in the state $A_p$ can be evaluated to $A_p(x)$, which is just the value of the function $A_p$ when you pass in the variable name $x$ as argument.

Hope that helps. For more details, lecture notes on operational semantics (e.g. these from Cambridge) will further explain the notation.

StackExchange Computer Science Q#83770, answer score: 6