Skip to content

Latest commit

 

History

History
 
 

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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.
  • The distinction between structural and computational rules.

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.