In this tutorial, we will show how to use the K formal semantic framework (http://kframework.org) to define your own programming languages, which is easy and fun. Specifically, the tutorial will cover the following topics:

• Use the BNF grammar notation to define programming language syntax;
• Define the computation configurations of the language, which consist of program code and its execution environment;
• Define the operational semantics of the language using rewrite rules.
• Use K to automatically generate the language tools, including a parser and an interpreter of the language.

We will be using a pedagogical and research language called FUN as an example, which captures the essence of the functional programming paradigm and includes many interesting language features such as user-defined data types, let/letrec constructs for defining recursive functions, pattern matching, and a callcc construct.

We highly recommend that the attendants of the tutorial download the K tools from its URL (https://github.com/kframework/k) and install it on their machines (instructions have been provided for Linux-like systems; for Windows, an installation instruction on fresh Windows Subsystem for Linux is provided).