TY - JOUR
T1 - An overview of the K semantic framework
AU - Roşu, Grigore
AU - Şerbǎnuţǎ, Traian Florin
N1 - Funding Information:
Acknowledgments. This research was supported by NSF Grants CCF-0916893, CNS-0720512, and CCF-0448501, by NASA contract NNL08AA23C, and by several Microsoft gifts. The authors would like to thank Mark Hills, Narciso Martí Oliet, Patrick Meredith, Peter Mosses, as well as the anonymous reviewers for insightful suggestions on earlier drafts of this paper. Warm thanks also go to the members of the FSL group at Urbana and Dorel Lucanu’s group in Iasi, Romania, who provided invaluable feedback during the last 7 years of research on K and applications. Last but not least, we are grateful to Gheorghe Pa˘un and Gheorghe Stefa˘nescu for noticing the interesting relationships between P-systems and K, and for encouraging us to write and submit this paper.
PY - 2010/8
Y1 - 2010/8
N2 - K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of configurations, computations and rules. Configurations organize the system/program 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; in particular, computations extend the original language or calculus syntax. K (rewrite) rules generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about. This distinction makes K a suitable framework for defining truly concurrent languages or calculi, even in the presence of sharing. Since computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted, K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions, or call/cc. This paper gives an overview of the K framework: what it is, how it can be used, and where it has been used so far. It also proposes and discusses the K definition of Challenge, a programming language that aims to challenge and expose the limitations of existing semantic frameworks.
AB - K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of configurations, computations and rules. Configurations organize the system/program 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; in particular, computations extend the original language or calculus syntax. K (rewrite) rules generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about. This distinction makes K a suitable framework for defining truly concurrent languages or calculi, even in the presence of sharing. Since computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted, K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions, or call/cc. This paper gives an overview of the K framework: what it is, how it can be used, and where it has been used so far. It also proposes and discusses the K definition of Challenge, a programming language that aims to challenge and expose the limitations of existing semantic frameworks.
UR - http://www.scopus.com/inward/record.url?scp=77955419874&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77955419874&partnerID=8YFLogxK
U2 - 10.1016/j.jlap.2010.03.012
DO - 10.1016/j.jlap.2010.03.012
M3 - Article
AN - SCOPUS:77955419874
SN - 1567-8326
VL - 79
SP - 397
EP - 434
JO - Journal of Logic Programming
JF - Journal of Logic Programming
IS - 6
ER -