Many-Sorted Natural Semantics

object-oriented programming languages can be described via inference
rules. Even though inference rules are the method of choice in the
description of functional languages, their use for the specification
of imperative and object-oriented languages is rather unusual.
Natural semantics is a specification method to describe the static and
dynamic semantics of programming languages based on inference rules.
We point out the limits of natural semantics and present the
many-sorted extensions which are necessary to specify imperative and
object-oriented proramming languages. Moreover, we show how the
semantic analysis can be generated from many-sorted natural semantics
specifications. Thereby, we can perform the generation of the semantic
analysis by using object-oriented libraries such that the resulting
semantic analysis is efficient. The correctness of the used
object-oriented library implies the correctness of the semantic
analysis.

Joint work with Wolf Zimmermann