# Examples of interesting semantics to study during a small project for a graduate Semantics course

I have been following the course Concrete Semantics with Isabelle/HOL. At some point we are given the task to verify a program/extend some semantic construction/prove some mathematical fact. I personally prefer to dive a little bit more into operational semantics, so adding new features to the IMP language is the way to go.

The classical extensions are non-determinism/parallel execution. These are described in a variety of books (Winskel, Hennessy or Nielson to cite only classical authors). However, I feel the treatment is rather limited and I'm not sure that can be turned into project, it looks more like a bunch of exercises.

So my question is are you aware of any simple but interesting extensions of the operational semantics approach to the study of a simple WHILE-program (such as IMP)? I would be looking specially for significant properties that can be proved in that semantics and illustrative examples that may be relevant.

• This question is a bit broad for CS.SE. Here we prefer questions having a definite answer. Still, it shows some effort, so I'm not going to vote-close it (but I wouldn't be surprised if others are). – chi Dec 20 '18 at 12:02

You could add more flow control to IMP, like (simple) exceptions, or break to exit early from a while loop.
You could add more complex data types, like pairs. Make it so that e.g. projecting a value out of a non-pair value causes a runtime error. Craft a (first-order) simple type system e.g. using T ::= int | (T*T) as types, and prove that "typeable programs do not go wrong", i.e. executing them never lead to runtime errors.
You could prove that a suitable restriction of IMP (say, sans while, or with a constrained while) is always terminating.