Bayle Shanks's website: proj-plbook-plChSemantics

Table of Contents for Programming Languages: a survey

Chapter : Semantics

Denotational

Operational

What else?

Effect analysis

The clearest intro i've seen: http://wingolog.org/archives/2014/05/18/effects-analysis-in-guile

Abstract interpretation

(If you are familiar with the mathematical idea of homomorphism, this is just an application of that)

If you are going to multiply two integers,

c = a * b

then you known that if sign(a) = +, sign(b) = +, then sign(c) = +, and similarly

sign(a) = + and sign(b) = - --> sign(c) = - sign(a) = - and sign(b) = + --> sign(c) = - sign(a) = - and sign(b) = - --> sign(c) = +

so, you could imagine an operator, call it multiply_sign in the domain {-,+} with this behavior. So you map the domain of integers to the domain of {-,+}, and map the multiplication operator * to multiply_sign. This allows you to know something about c without calculating it directly (in particular, if you know the sign of a and of b, you can know the sign of c).

...

Todo: big step, small step, etc Semantics of programming languages

Links:

---

Unifying Theories of Programming (UTP) by Hoare and He. https://en.wikipedia.org/wiki/Unifying_Theories_of_Programming

---

Operational semantics: Structural operational semantics: big step semantics vs. small step semantics

In small-step semantics, we write inference rules for individual reduction steps.

For example, if <e, state> denotes expression 'e' in context 'context', one rule might be (given in sequent notation):

   <e1, s> -> <e1', s>

and another might be

   <e1, s> -> <e1', s>

In big-step semantics, each 'big step' is just the result of combining many small-step transitions into one step.

For example, we might say:

   <e1, s> => <e1', s>   <e2, s> => <e2', s>

         <e1 + e2, s> => <e1' + e2', s>

where => denotes a 'big arrow' (usually denoted by a big downward-facing arrow) and "a => b" means "after applying one or more small-steps, a can be reduced to b, and cannot be further reduced" (todo: check: is that actually what it formally means?).

For terminating reduction chains, the big-step and small-step semantics of a language should agree (and people try to prove this, for specific semantics for specific languages).

"big-step semantics cannot talk directly about nontermination" If <e, s> does not terminate, then there is no <e2, s2> such that <e,s> => <e2, s2> [1]

" Comparison of big-step vs. small-step SOS

5.1 Small-step

Small-step semantics can clearly model more complex features, like concurrency, divergence, and runtime errors.
Although one-step-at-a-time evaluation is useful for proving certain properties, in some cases it is unnecessary work to talk about each small step.

5.2 Big-step

Big-step semantics more closely models a recursive interpreter.
Big steps in reasoning make it quicker to prove some things, because there are fewer rules. The “boring” rules of the small-step semantics that specify order of evaluation are folded into the way that state is threaded through the big-step rules.
Because evaluation skips over intermediate steps, all programs without final configurations (infinite loops, errors, stuck configurations) look the same. So you sometimes can’t prove things related to these kinds of configurations. " -- [2]

Links:

http://www.cs.cornell.edu/courses/cs6110/2009sp/lectures/lec05-fa07.pdf