Section 2: Intermediate K Concepts

The goal of this second section is to supplement a beginning developer's knowledge of K after they have gained a basic understanding of K. Each lesson in this section can be completed independently in order to learn about a particular facet of the K language. The lessons are written to provide basic understanding of less commonly-used features of K to someone who is still learning K. For more complete references of these features, the reader ought to consult the User Manual.

The reader ought to be able to complete lessons in this section as needed in order to learn about specific features of interest, but if desired, can also complete the entire section in one go. Someone who has completed this entire section ought to be able to read and understand most K specifications, as well as write their own specifications of some complexity, and use them to perform most common K-related tasks. They can then read about specific lessons in Section 3: Advanced K Concepts if they want to learn more.

Table of Contents

  1. Macros, Aliases, and Anywhere Rules
  2. Fresh Constants
  3. KLabels and Abstract Syntax
  4. Overloaded Symbols
  5. Matching Logic Connectives and #Or Patterns
  6. Function Context
  7. Record Productions and Named Nonterminals
  8. #fun and #let
  9. #as patterns
  10. The Matching Operators, :=K and :/=K
  11. Uncommon Evaluation Order Concepts
  12. IEEE 754 Floating Point and Fixed Width Integers
  13. Alpha-renaming-aware Substitution
  14. File I/O
  15. String Buffers and Byte Sequences
  16. The Intermediate Language of K, KORE
  17. Debugging Proofs using the Haskell Backend REPL