Part 2: Defining IMP

Here you will learn how to define a very simple imperative language in K and the basics of how to work with configurations, cells, and computations. Specifically, you will learn the following:

• How to define languages using multiple modules.
• How to define sequentially strict syntactic constructs.
• How to use K's syntactic lists.
• How to define, initialize and configure configurations.
• How the language syntax is swallowed by the builtin K syntactic category.
• The additional syntax of the K syntactic category.
• How the strictness annotations are automatically desugared into rules.
• The first steps of the configuration abstraction mechanism.

Like in the previous tutorial, this folder contains several lessons, each adding new features to IMP. Do them in order. Also, make sure you completed and understood the previous tutorial.