Semantic Framework
pdf
epub
mobi
html
Download
Homepage
Install K
Pyk Documentation
K Tutorial
Section 1: Basic K Concepts
Lesson 1.1: Setting up a K Environment
Lesson 1.2: Basics of Functional K
Lesson 1.3: BNF Syntax and Parser Generation
Lesson 1.4: Disambiguating Parses
Lesson 1.5: Modules, Imports, and Requires
Lesson 1.6: Integers and Booleans
Lesson 1.7: Side Conditions and Rule Priority
Lesson 1.8: Literate Programming with Markdown
Lesson 1.9: Unparsing and the format and color attributes
Lesson 1.10: Strings
Lesson 1.11: Casting Terms
Lesson 1.12: Syntactic Lists
Lesson 1.13: Basics of K Rewriting
Lesson 1.14: Defining Evaluation Order
Lesson 1.15: Configuration Declarations and Cell Nesting
Lesson 1.16: Maps, Semantic Lists, and Sets
Lesson 1.17: Cell Multiplicity and Cell Collections
Lesson 1.18: Term Equality and the Ternary Operator
Lesson 1.19: Debugging with GDB or LLDB
Lesson 1.20: K Backends and the Haskell Backend
Lesson 1.21: Unification and Symbolic Execution
Lesson 1.22: K Deductive Verification
Section 2: Intermediate K Concepts
Lesson 2.1: Macros, Aliases, and Anywhere Rules
Lesson 2.2: Fresh Constants
Lesson 2.3: KLabels and Abstract Syntax
Lesson 2.4: Overloaded Symbols
Lesson 2.5: Matching Logic Connectives and #Or Patterns
Lesson 2.6: Function Context
Lesson 2.7: Record Productions and Named Nonterminals
Lesson 2.8: #fun and #let
Lesson 2.9: #as Patterns
Lesson 2.10: The Matching Operators, :=K and :/=K
Lesson 2.11: Uncommon Evaluation Order Concepts
Lesson 2.12: IEEE 754 Floating Point and Fixed Width Integers
Lesson 2.13: Alpha-renaming-aware Substitution
Lesson 2.14: File I/O
Lesson 2.15: String Buffers and Byte Sequences
Lesson 2.16: The Intermediate Language of K, KORE
Lesson 2.17: Debugging Proofs using the Haskell Backend REPL
K User Manual
K Cheat Sheet
K Tool Reference
K Builtins
domains
kast
prelude
ffi
json
rat
substitution
unification
K PL Tutorial
K Overview
Learning K
Part 1: Defining LAMBDA
Lesson 1, LAMBDA: Syntax Modules and Basic K Commands
Lesson 2, LAMBDA: Module Importing, Rules, Variables
Lesson 3, LAMBDA: Evaluation Strategies using Strictness
Lesson 4, LAMBDA: Generating Documentation; Latex Attributes
Lesson 5, LAMBDA: Adding Builtins; Side Conditions
Lesson 6, LAMBDA: Selective Strictness; Anonymous Variables
Lesson 7, LAMBDA: Derived Constructs; Extending Predefined Syntax
Lesson 8, LAMBDA: Multiple Binding Constructs
Lesson 9, LAMBDA: A Complete and Commented Definition
Part 2: Defining IMP
Lesson 1, IMP: Defining a More Complex Syntax
Lesson 2, IMP: Defining a Configuration
Lesson 3, IMP: Computations, Results, Strictness; Rules Involving Cells
Lesson 4, IMP: Configuration Abstraction, Part 1; Types of Rules
Lesson 5, IMP: Completing and Documenting IMP
Part 3: Defining LAMBDA++
Lesson 1, LAMBDA++: Abrupt Changes of Control
Lesson 2, LAMBDA++: Semantic (Non-Syntactic) Computation Items
Lesson 3, LAMBDA++: Reusing Existing Semantics
Lesson 4, LAMBDA++: Do Not Reuse Blindly!
Lesson 5, LAMBDA++: More Semantic Computation Items
Lesson 6, LAMBDA++: Wrapping Up and Documenting LAMBDA++ (environment-based)
Part 4: Defining IMP++
Lesson 1, IMP++: Extending/Changing an Existing Language Syntax
Lesson 2, IMP++: Configuration Refinement; Freshness
Lesson 3, IMP++: Tagging; Superheat/Supercool Kompilation Options
Lesson 4, IMP++: Semantic Lists; Input/Output Streaming
Lesson 5, IMP++: Deleting, Saving and Restoring Cell Contents
Lesson 6, IMP++: Adding/Deleting Cells Dynamically; Configuration Abstraction, Part 2
Lesson 7, IMP++: Everything Changes: Syntax, Configuration, Semantics
Lesson 8, IMP++: Wrapping up Larger Languages
Part 5: Defining Type Systems
Lesson 1, Type Systems: Imperative, Environment-Based Type Systems
Lesson 2, Type Systems: Substitution-Based Higher-Order Type Systems
Lesson 3, Type Systems: Environment-Based Higher-Order Type Systems
Lesson 4, Type Systems: A Naive Substitution-Based Type Inferencer
Lesson 5, Type Systems: A Naive Environment-Based Type Inferencer
Lesson 6, Type Systems: Parallel Type Checkers/Inferencers
Lesson 7, Type Systems: A Naive Substitution-based Polymorphic Type Inferencer
Lesson 8, Type Systems: A Naive Environment-based Polymorphic Type Inferencer
Lesson 9, Type Systems: Let-Polymorphic Type Inferencer (Damas-Hindley-Milner)
Learning Language Design and Semantics using K
Part 7: SIMPLE: Designing Imperative Programming Languages
Lesson 1, SIMPLE untyped
Lesson 2, SIMPLE typed static
Lesson 3, SIMPLE typed dynamic
Part 8: KOOL: Designing Object-Oriented Programming Languages
Lesson 1, KOOL untyped
Lesson 2, KOOL typed dynamic
Lesson 3, KOOL typed static
Part 9: FUN: Designing Functional Programming Languages
Lesson 1, FUN untyped, Environment-Based
Lesson 2, FUN untyped, Substitution-Based
Lesson 3, FUN polymorphic type inferencer
Part 10: LOGIK: Designing Logic Programming Languages
Lesson 1, LOGIK
Projects using K
Revise the change of
S1 S2
into
S1:Stmt S2:Stmt
, if needed; only
S2
really needs to be sorted.
