Section 1: Basic K Concepts

The goal of this first section of the K tutorial is to teach the basic principles of K to someone with no prior experience with K as a programming language. However, this is not written with the intended audience of someone who is a complete beginner to programming. We are assuming that the reader has a firm grounding in computer science broadly, as well as that they have experience writing code in functional programming languages before.

By the end of this section, the reader ought to be able to write specifications of simple languages in K, use these specifications to generate a fast interpreter for their programming language, as well as write basic deductive program verification proofs over programs in their language. This should give them the theoretical grounding they need to begin expanding their knowledge of K in Section 2: Intermediate K Concepts.

To begin this section, refer to Lesson 1.1: Setting up a K Environment.