K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. K rewrite rules make it explicit which parts of the term are read-only, write-only, read-write, or unused. This makes K suitable for defining truly concurrent languages even in the presence of sharing. Computations are represented as syntactic extensions of the original language abstract syntax, using a nested list structure which sequentializes computational tasks, such as program fragments. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions, or call/cc.
K Tool Download
- Install from the latest K GitHub Release.
- Try our Editor Support page for links to K syntax highlighting definitions for various popular editors/IDEs. Please feel free to contribute.
- Build or browse the code on GitHub, where you can also report bugs.
- Discord Server: Most direct way to get support.
- Matrix Room: Another way to get support.
- Telegram: for newsletters and general announcements.
- A set of reference implementations and tutorials for common programming language features and paradigms is available, although parts of these implementations may not be fully up to date with modern K features.
- Read some papers about K on the Formal Systems Laboratory (FSL).
- Matching logic webpage at UIUC (USA).
- A ten-minute overview video slide presentation.
- A ninety-minute tutorial video, given at ETAPS'16.
- [Optional] A high-level interview about rewrite-based semantics (Wolfram Schulte interviews Grigore Rosu at ICSE'11.