K Prover swMATH ID: 32257 Software Authors: Roşu, Grigore et.al Description: K Prover. An overview of the K semantic framework. 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. Homepage: http://www.kframework.org/index.php/Main_Page Source Code: https://github.com/kframework/k Related Software: Maude; K tool; z3; MMT; JavaFAN; K-Java; PLT Redex; Coq; ACL2; Centaur; KOOL; K-Maude; Java+ITP; Stratego; Ott; Toolchain; CafeOBJ; ML; CASL; Isabelle/HOL Cited in: 46 Documents Further Publications: http://www.kframework.org/index.php/K_Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year An overview of the K semantic framework. Zbl 1214.68188Roşu, Grigore; Şerbănuţă, Traian Florin 2010 all top 5 Cited by 58 Authors 23 Roşu, Grigore 15 Şerbănuţă, Traian Florin 8 Lucanu, Dorel 8 Rusu, Vlad 6 Arusoaie, Andrei 6 Ştefănescu, Andrei 5 Meseguer Guaita, José 4 Ciobâcă, Ştefan 3 Hills, Mark 2 Ellison, Chucky 2 Mereuta, Radu 2 Moore, Brandon M. 2 Ştefănescu, Gheorghe 1 Bettini, Lorenzo 1 Biernacka, Małgorzata 1 Bogdanas, Denis 1 Bugliesi, Michele 1 Calzavara, Stefano 1 Charatonik, Witold 1 Cheney, James 1 Chira, Camelia 1 Cirstea, Horatiu 1 Dinu, Liviu Petrişor 1 Dong, JinSong 1 Fava, Daniel Schnetzer 1 Focardi, Riccardo 1 Guan, Zhichao 1 Gunter, Elsa L. 1 Haustermann, Michael 1 Hoa, Koh Chuen 1 Hou, Zhe 1 Hu, Zhenjiang 1 Johansen, Christian 1 Lermusiaux, Pierre F. J. 1 Li, Liyi 1 Liu, Yang 1 Lochbihler, Andreas 1 Moldt, Daniel 1 Momigliano, Alberto 1 Moreau, Pierre-Etienne 1 Mosses, Peter D. 1 Mosteller, David 1 Nowak, David E. 1 Owe, Olaf 1 Pfenning, Frank 1 Sanán, David 1 Schulte, Wolfram 1 Sculthorpe, Neil 1 Simmons, Robert jun. 1 Steffen, Martin 1 Stolz, Volker 1 Tiu, Alwen Fernanto 1 van Binsbergen, L. Thomas 1 Weißbach, Mandy 1 Xiao, Yushuo 1 Yang, Ziyi 1 Zielińska, Klara 1 Zimmermann, Wolf all top 5 Cited in 11 Serials 6 Journal of Logical and Algebraic Methods in Programming 3 The Journal of Logic and Algebraic Programming 2 Information and Computation 2 Journal of Automated Reasoning 2 Logical Methods in Computer Science 1 Revue Roumaine de Mathématiques Pures et Appliquées 1 Journal of Symbolic Computation 1 Formal Aspects of Computing 1 Higher-Order and Symbolic Computation 1 Theory and Practice of Logic Programming 1 Computer Languages, Systems & Structures Cited in 3 Fields 46 Computer science (68-XX) 16 Mathematical logic and foundations (03-XX) 1 Biology and other natural sciences (92-XX) Citations by Year