Section 1: Basic K Concepts

In this first section you'll learn the basic principles of K. We assume you've got no prior experience with K as programming language, so we teach you everything.

By the end of this section, you'll be able to define a simple language in K and use its specifications to generate a fast interpreter for it. You'll also know how to write basic deductive program verification proofs over programs writen in your language. You'll be all set to dwelve into more advanced stuff coming up in the next section Section 2: Intermediate K Concepts.

First things first, you need to set up K environment on your machine. Lesson 1.1: Setting up K Environment.