Main Page
From K Framework
is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program. Computations extend the original language abstract syntax. K (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes K suitable for defining truly concurrent languages even in the presence of sharing. 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.
Quick Overview
- A ten-minute overview video slide presentation.
- A five-minute video demo of the K Tool (download the tool below); a K tutorial also available below.
- The documented K semantics of
LAMBDA, IMP and KOOL (generated by the K Tool); more semantics available below.
- [Optional] A high-level interview about rewrite-based semantics (Wolfram Schulte interviews Grigore Rosu at ICSE'11).
K Tool Download and Online Interface
- The provided K tool binaries run best on Linux and OS X. Although they can run directly on Windows too, this process could be quite slow due to using Cygwin emulation. To alleviate that, we offer the KVM - The K Virtual Machine solution.
- The source code (Java) is available on Googlecode, where you can also report bugs (please do so).
- An experimental online interface to the K tool is also available (in Romania).
- Ask general questions at info@k-framework.org and subscribe to the K user list for news on major tool updates and questions.
Learn K
- Do the K Tutorial !
- Consult the documented semantics of the languages in the K tool distribution.
- Read some papers about K (click on Publications in the left tab).
Links
K and matching logic webpage at UIUC (USA).
K webpage at UAIC (Romania).
Matching logic webpage at UIUC (USA).
