Abstract
K is a rewriting-based framework for defining programming languages. K-Maude is a tool implementing K on top of Maude. K-Maude provides an interface accepting K modules along with regular Maude modules and a collection of tools for transforming K language definitions into Maude rewrite theories for execution or analysis, or into LaTeX for documentation purposes. The current K-Maude prototype was successfully used in defining several languages and language analysis tools, both for research and for teaching purposes. This paper describes the K-Maude tool, both from a user and from an implementer perspective.
Supported in part by NSF grants CCF-0916893, CNS-0720512, and CCF-0448501, NASA contract NNL08AA23C, a Samsung SAIT grant, and several Microsoft gifts.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96(1), 217–248 (1992)
Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Kahn, G.: Natural semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoretical Computer Science 373(3), 213–237 (2007)
Mosses, P.D.: Modular structural operational semantics. Journal of Logic and Algebraic Programming (60-61), 195–228 (2004)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming (60-61), 17–139 (2004)
Roşu, G., Ellison, C., Schulte, W.: Matching logic: An alternative to Hoare/Floyd logic. In: AMAST 2010. LNCS, Springer, Heidelberg (2010)
Roşu, G.: K: a rewrite-based framework for modular language design, semantics, analysis and implementation. Tech. Rep. UIUCDCS-R-2006-2802, University of Illinois (2006)
Roşu, G., Schulte, W., Şerbănuţă, T.F.: Runtime verification of C memory safety. In: Peled, D. (ed.) RV 2009. LNCS, vol. 5779, pp. 132–151. Springer, Heidelberg (2009)
Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming (2010), doi:10.1016/j.jlap.2010.03.012
Şerbănuţă, T.F., Roşu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Information and Computation 207, 305–340 (2009)
Strachey, C., Wadsworth, C.P.: Continuations: A mathematical semantics for handling full jumps. Higher-Order and Symbolic Computation 13(1/2), 135–152 (2000)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Şerbănuţă, T.F., Roşu, G. (2010). K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. In: Ölveczky, P.C. (eds) Rewriting Logic and Its Applications. WRLA 2010. Lecture Notes in Computer Science, vol 6381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16310-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-16310-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16309-8
Online ISBN: 978-3-642-16310-4
eBook Packages: Computer ScienceComputer Science (R0)