Aleksy Schubert
Warsaw University
Formalisation of a frame stack semantics for a Java-like language
We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Feather-weight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods.
On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a complex value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the un- typed version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it.
