An overview of the K semantic framework
Grigore Ro,su, Traian Florin ,Serb˘anu,t˘a

The Journal of Logic and Algebraic Programming 79 (2010) 397–434

abstract

K is an executable semantic framework in which programming languages, calculi, as well
as type systems or formal analysis tools can be defined, making use of configurations, computations
and rules. Configurations organize the system/program state in units called cells,
which are labeled and can be nested. Computations carry “computational meaning” as special
nestedlist structures sequentializingcomputational tasks, suchas fragments of program;
in particular, computations extend the original language or calculus syntax. K (rewrite) rules
generalize conventional rewrite rules by making explicit which parts of the term they read,
write, or do not care about. This distinction makes K a suitable framework for defining truly
concurrent languages or calculi, even in the presence of sharing. Since computations can
be handled like any other terms in a rewriting environment, that is, they can be matched,
moved from one place to another in the original term, modified, or even deleted, K is particularly
suitable for defining control-intensive language features such as abrupt termination,
exceptions, or call/cc.
This paper gives an overview of the K framework: what it is, how it can be used, and
where it has been used so far. It also proposes and discusses the K definition of Challenge,
a programming language that aims to challenge and expose the limitations of existing semantic
frameworks.

An overview of the K semantic framework.pdf

看不懂！