|Abstract:||K is an algebraic framework for defining programming languages. It consists of a technique and of a specialized and highly optimized notation. The K-technique, which can be best explained in terms of rewriting modulo equations or in terms of rewriting logic, is based on a first-order representation of continuations with intensive use of matching modulo associativity, commutativity and identity. The K-notation consists of a series of high-level conventions that make the programming language definitions intuitive, easy to understand, to read and to teach, compact, modular and scalable. One important notational convention is based on context transformers, allowing one to automatically synthesize concrete rewrite rules from more abstract definitions once the concrete structure of the state is provided, by .completing. the contexts in which the rules should apply. The K framework is introduced by defining FUN, a concurrent higher-order programming language with parametric exceptions. A rewrite logic definition of a programming language can be executed on rewrite engines, thus providing an interpreter for the language for free, but also gives an initial model semantics, amenable to formal analysis such as model checking and inductive theorem proving. Rewrite logic definitions in K can lead to automatic, correct-by-construction generation of interpreters, compilers and analysis tools.