K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation - Version 2 -

Rosu, Grigore

Permalink

https://hdl.handle.net/2142/11284 Copy

Description

Title

K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation - Version 2 -

Author(s)

Rosu, Grigore

Issue Date

2006-12

Keyword(s)

programming languages

Abstract

K is an algebraic framework for defining programming languages. It consists of a technique and of a specialized and highly optimized notation. The K-technique, which can be best explained in terms of rewriting modulo equations or in terms of rewriting logic, is based on a first-order representation of continuations with intensive use of matching modulo associativity, commutativity and identity. The K-notation consists of a series of high-level conventions that make the programming language definitions intuitive, easy to understand, to read and to teach, compact, modular and scalable. One important notational convention is based on context transformers, allowing one to automatically synthesize concrete rewrite rules from more abstract definitions once the concrete structure of the state is provided, by .completing. the contexts in which the rules should apply. The K framework is introduced by defining FUN, a concurrent higher-order programming language with parametric exceptions. A rewrite logic definition of a programming language can be executed on rewrite engines, thus providing an interpreter for the language for free, but also gives an initial model semantics, amenable to formal analysis such as model checking and inductive theorem proving. Rewrite logic definitions in K can lead to automatic, correct-by-construction generation of interpreters, compilers and analysis tools.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11284

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections