From FSL
Jump to: navigation, search

Authors: Patrick Meredith, Mark Hills, and Grigore Rosu

Scheme is a functional (though impure) language, with a first class representation of continuations. In Scheme, code and data have a unified representation; because of this, Scheme has some of the best meta-programming tools of any language. K-Scheme is a formal, executable, definition of Scheme, using the K language definitional style within (the equational fragment of) rewriting logic. It has been inspired from an earlier definition of LISP, called LISB; superficial changes include, but are not limited to: macros by example, vectors, true strings, improper lists, scheme-style variable arguments, call-with-current-continuation (and its relatives call-with-values and dynamic-wind), quasiquotation, and first class environments.

K-Scheme can serve at least two purposes:

  • as a formal, equational definition of Scheme complementary to the informal one in the R5RS report, and
  • as a platform for experimentation with new features and future versions of Scheme.

K-Scheme is available for download and can also be executed online:

Related projects: K; Rewriting Logic Semantics


News and Change Logs

  • 2007-10-10: K-Scheme version 1.3 was released. Improvements over 1.2:
  • Non-deterministic evaluation of sub terms in function application forms
  • Non-deterministic evaluation of unquote forms in quasiquote forms
  • Non-deterministic copy for quote
  • Better error messages
  • 2007-08-13: K-Scheme version 1.2 was released. Improvements over 1.1:
  • Scheme defined functions moved into library, initialization module removed.
  • Most keywords are now treated as normal identifiers, simplifying the definition.
  • New parser written using ocamlyac and ocamllex fixes old shortcomings
  • 2007-07-23: K-Scheme version 1.1 was released. Improvements over 1.0:
  • Added internal defines.
  • Definition made cleaner.
  • Built-in procedures and keywords are now properly bound in the global environment rather than the local.
  • 2007-06-30: K-Scheme version 1.0 was released. Known limitations:
  • Current K-Scheme definition uses the K technique, but it "implements" it using plain rewriting logic in Maude, taking full advantage of some current Maude specifics, such as, for example, that the equations are applied in order; these assumptions simplify K-Scheme's definitions and are easy to eliminate if one is interested in using our definition for other purposes, such as formal property proving.
  • To make our definition Maude-friendly, the Scheme syntax was adjusted; however, the download package, as well as K-Scheme's online iterface (Online-sm.JPG), use a parser to automatically translate a Scheme program into a K-Scheme program.
  • Parser occasionally fails; it should be modified in the near future.
  • Lacks internal defines and a few library procedures.
  • Let label not defined.
  • Macros incomplete, but functional for many important cases (they may be migrated to operate on the internal representation rather than syntax at a future date to support staged macro evaluation -- needed to properly support marcos within eval, or even nested eval, expressions).

Download and Installation

Online-sm.JPG before download!

The formal Maude definition of K-Scheme is available below, as well as the parser and examples:

All one needs to do is to start Maude and then load the .maude file in the package above. The parser requires Python. It accepts a scheme file and outputs K-Scheme code to standard out.


Detailed documentation will be posted here soon.

The Maude definition in the download package above is documented and can be most useful.


Publications on K-Scheme are available below in reverse chronological order. The original tech report was modified to form the submission to the Scheme workshop. The last tech report explains newer additions to the definition, and is more concise, using the actual K notation rather than the implementation language.

A K Definition of Scheme 
Patrick Meredith, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2007-2907, October 2007
An Executable Rewriting Logic Semantics of K-Scheme 
Patrick Meredith, Mark Hills and Grigore Rosu
8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007

External Links

  • R5RS provides a comprehensive informal definition of the current version of Scheme.
Personal tools