An overview of the K semantic framework. (English) Zbl 1214.68188

Summary: 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.


68Q42 Grammars and rewriting systems
68N15 Theory of programming languages
68Q55 Semantics in the theory of computing
Full Text: DOI Link


[1] Alba-Castro, M.; Alpuente, M.; Escobar, S., Automatic certification of Java source code in rewriting logic, (), 200-217
[2] M. Alba-Castro, M. Alpuente, S. Escobar, P. Ojeda, D. Romero, A tool for automated certification of Java source code in Maude, in: Proceedings of the Eighth Spanish Conference on Programming and Computer Languages (PROLE 2008), Electronic Notes Theoretical Computer Science, vol. 248, 2009, pp. 19-29.
[3] Banâtre, J.-P.; Métayer, D.L., The GAMMA model and its discipline of programming, Sci. comput. programming, 15, 1, 55-77, (1990) · Zbl 0715.68054
[4] Barbuti, R.; Maggiolo-Schettini, A.; Milazzo, P.; Troina, A., A calculus of looping sequences for modelling microbiological systems, Fundam. inform., 72, 1-3, 21-35, (2006) · Zbl 1101.92021
[5] Berry, G.; Boudol, G., The chemical abstract machine, Theoret. comput. sci., 96, 1, 217-248, (1992) · Zbl 0747.68013
[6] P. Bottoni, C. Martín-Vide, G. Păun, G. Rozenberg, Membrane systems with promoters/inhibitors, Acta Inform. 38(10), 695-720. · Zbl 1034.68038
[7] Clavel, M.; Durán, F.; Eker, S.; Meseguer, J.; Lincoln, P.; Martí-Oliet, N.; Talcott, C., All about maude, A high-performance logical framework, Lecture notes in computer science, vol. 4350, (2007), Springer
[8] O. Danvy, L. R. Nielsen, Refocusing in reduction semantics, RS RS-04-26, BRICS, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, this report supersedes BRICS report RS-02-04. A Preliminary Version Appears in the Informal Proceedings of the Second International Workshop on Rule-Based Programming, RULE 2001, Electronic Notes in Theoretical Computer Science, vol. 59.4, November 2004.
[9] Ehrig, H., Introduction to the algebraic theory of graph grammars (a survey), (), 1-69
[10] C. Ellison, T.F. Șerbănută, G. Roșu, A rewriting logic approach to type inference, in: Recent Trends in Algebraic Development Techniques — 19th International Workshop, WADT 2008, Pisa, Italy, June 13-16, 2008, Revised Selected Papers, Lecture Notes in Computer Science, vol. 5486, Springer, 2009, pp. 135-151.
[11] Farzan, A.; Chen, F.; Meseguer, J.; Roșu, G., Formal analysis of Java programs in javafan, (), 501-505 · Zbl 1103.68611
[12] M. Felleisen, D.P. Friedman, Control operators, the SECD-machine, and the lambda-calculus, in: 3rd Working Conference on the Formal Description of Programming Concepts, Ebberup, Denmark, 1986, pp. 193-219.
[13] Giavitto, J.-L.; Michel, O., MGS: a rule-based programming language for complex objects and collections, (), 286-304 · Zbl 1268.68041
[14] J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, J.-P. Jouannaud, Introducing OBJ, in: J. Goguen (Ed.), Applications of Algebraic Specification using OBJ, Cambridge, 1993.
[15] M. Hills, F. Chen, G. Roșu, A rewriting logic approach to static checking of units of measurement in C, in: Proceedings of the 9th International Workshop on Rule-Based Programming (RULE’08), ENTCS, Elsevier, in press.
[16] M. Hills, T. B. Aktemur, G. Roșu, An executable semantic definition of the Beta language using rewriting logic, Tech. Rep. UIUCDCS-R-2005-2650, Department of Computer Science, University of Illinois at Urbana-Champaign, 2005.
[17] Hills, M.; Roșu, G., Towards a module system for K, (), 187-205
[18] M. Hills, T. F. Șerbănută, G. Roșu, A rewrite framework for language definitions and for generation of efficient interpreters, in: Proceedings of the 6th International Workshop on Rewriting Logic and its Applications (WRLA’06), Electronic Notes in Theoretical Computer Science, vol. 176, Elsevier Science, 2007, pp. 215-231, also appeared as Technical Report UIUCDCS-R-2005-2667, December 2005.
[19] Hills, M.; Roșu, G., A rewriting approach to the design and evolution of object-oriented languages, (), 827-828
[20] Hills, M.; Roșu, G., KOOL: an application of rewriting logic to language prototyping and analysis, (), 246-256
[21] M. Hills, G. Roșu, On formal analysis of OO languages using rewriting logic: designing for performance, in: Proceedings of the 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS’07), LNCS, vol. 4468, Springer, 2007, pp. 107-121, also appeared as Technical Report UIUCDCS-R-2007-2809, January 2007.
[22] Kahn, G., Natural semantics, (), 22-39 · Zbl 0657.68079
[23] Meseguer, J.; Roșu, G., Rewriting logic semantics: from language specifications to formal analysis tools, (), 1-44 · Zbl 1126.68464
[24] Meseguer, J.; Roșu, G., The rewriting logic semantics project, Theoret. comput. sci., 373, 3, 213-237, (2007) · Zbl 1111.68068
[25] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. comput. sci., 96, 1, 73-155, (1992) · Zbl 0758.68043
[26] Meseguer, J., Rewriting logic as a semantic framework for concurrency: a progress report, (), 331-372
[27] Milner, R.; Tofte, M.; Harper, R.; Macqueen, D., The definition of standard ML (revised), (1997), MIT Press Cambridge, MA, USA
[28] Mosses, P.D., Pragmatics of modular SOS, (), 21-40 · Zbl 1275.68086
[29] Mosses, P.D., Modular structural operational semantics, J. logic algebraic programming, 60-61, 195-228, (2004) · Zbl 1072.68061
[30] G.R. Patrick Meredith, Mark Hills, An executable rewriting logic semantics of K-Scheme, in: D. Dube (Ed.), Proceedings of the 2007 Workshop on Scheme and Functional Programming (SCHEME’07), Technical Report DIUL-RT-0701, Laval University, 2007, pp. 91-103.
[31] Păun, G., Computing with membranes, J. comput. syst. sci., 61, 108-143, (2000)
[32] Păun, A.; Păun, G., The power of communication: P systems with symport/antiport, New gener. comput., 20, 3, 295-305, (2002)
[33] Plotkin, G.D., A structural approach to operational semantics, J. logic algebraic programming, 60-61, 17-139, (2004), Original version: University of Aarhus Technical Report DAIMI FN-19, 1981 · Zbl 1082.68062
[34] G. Roșu, CS322, Fall 2003 - Programming Language Design: Lecture Notes, Tech. Rep. UIUCDCS-R-2003-2897, Department of Computer Science, University of Illinois at Urbana-Champaign, Lecture Notes of a Course Taught at UIUC, December 2003.
[35] G. Roșu, Programming Languages—A Rewriting Approach—, draft. Accessible online at: <http://fsl.cs.uiuc.edu/pub/pl.pdf>.
[36] G. Roșu, K: a rewriting-based framework for computations – preliminary version, Tech. Rep. Department of Computer Science UIUCDCS-R-2007-2926 and College of Engineering UILU-ENG-2007-1827, University of Illinois at Urbana-Champaign, 2007.
[37] G. Roșu, W. Schulte, Matching logic — extended report, Tech. Rep. Department of Computer Science UIUCDCS-R-2009-3026, University of Illinois at Urbana-Champaign, January 2009.
[38] G. Roșu, C. Ellison, W. Schulte, From rewriting logic executable semantics to matching logic program verification, Tech. Rep. http://hdl.handle.net/2142/13159, University of Illinois (July 2009). http://hdl.handle.net/2142/13159.
[39] G. Roșu, W. Schulte, T.F. Șerb&abreve;nut&abreve;, Runtime verification of C memory safety, in: Runtime Verification (RV’09), Lecture Notes in Computer Science, vol. 5779, 2009, pp. 132-152.
[40] Șerb&abreve;nut&abreve;, T.F.; Roșu, G.; Meseguer, J., A rewriting logic approach to operational semantics, Inform. comput., 207, 305-340, (2009)
[41] T.F. Șerb&abreve;nut&abreve;, G. Roșu, K-Maude: a rewriting based tool for semantics of programming languages, in: Proceedings of the 8th International Workshop on Rewriting Logic and its Applications (WRLA’10), Lecture Notes in Computer Science, in press.
[42] Șerb&abreve;nut&abreve;, T.F.; Stefanescu, G.; Roșu, G., Defining and executing P systems with structured data in K, (), 374-393 · Zbl 1196.68084
[43] Wright, A.K.; Felleisen, M., A syntactic approach to type soundness, Inform. comput., 115, 1, 38-94, (1994) · Zbl 0938.68559
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.