The K Framework (https://kframework.org/) provides a set of tools for developing programming languages. By writing a single description of your language’s syntax and operational semantics, you can use K to automatically extract a parser, interpreter, and symbolic execution engine (and many more) for your language. This approach scales: K implementations have been built for many mainstream programming languages (C, Rust, Java, Python, EVM to name a few), and K is used in practice every day for real verification problems.

This tutorial is aimed at anyone who is interested in programming language implementation or program verification, and will have three main parts:

1. We’ll cover setting up a K development environment, and the basics of writing simple K code.

2. Then, we’ll move on to defining the syntax and operational semantics of a simple imperative language in K. We’ll cover the most important parts of the K developer tooling and APIs here.

3. Finally, with our language definition in hand, we can begin taking advantage of K’s support for deductive verification to write some simple proofs over programs.

By the end of the tutorial, the aim is for attendees to be able to implement and verify their next research DSL or language using K.