Some papers define an operational semantics of a programming language. That is nice, but what makes such a semantics fit for the purpose?An idea is to have a progress theorem, i.e. well-formed expression is either a value or a reduction can take placeanother is type preservation, that an reduction preserves the type of an expression.What else is a test for the adequateness of a semantics? What should I prove about it?
What makes an operational semantics good?
operational semantics