Formal Systems Laboratory

SETSS'19 Lecture Notes on K

Abstract. We give an overview on the applications and foundations of the K language framework, a semantic framework for programming languages and formal analysis tools. K represents a 20-year effort in pursuing the ideal language framework vision, where programming languages must have formal definitions, and tools for a given language, such as parsers, interpreters, compilers, semantic-based debuggers, state-space explorers, model checkers, deductive program verifiers, etc., can be derived from just one reference formal definition of the language, which is executable, and no other semantics for the same language should be needed. The correctness of the languages tools is guaranteed on a case-by-case basis by proof objects, which encode rigorous mathematical proofs as certificates for every individual tasks that the tools do and can be mechanically checked by third-party proof checkers.