CinK – an exercise on how to think in K

CinK is a kernel of the C++ language we used to experiment with K. The language is used as an working example
for teaching classes and is refered in several research papers.
We assume the reader is already familiar with the K Framework and the K tool; we here share our experiece in
defining languages with some specific features, such as C++. In giving semantics to the language we keep as close
as possible to the C++ manual (version 2011). Therefore, for many constructs, the semantics rules are preceded
by a quoted text including the semantics description given in the manual.
CinK is defined in several iterations, each iteration being a incremental contribution. Each iteration can be
compiled and executes as a stand-alone definition.

Sidebar