IsaK-static: A complete static semantics of K

Research output: Chapter in Book/Report/Conference proceedingConference contribution


K[1] is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. K supports a module design for programming language specifications, with different language features separated in different modules. This is supported through a subsort system and K features called localization and concision. By these features and other features, language specifications can be defined in K effectively. In this paper we define a complete static semantics of K named IsaK-Static, in the interactive theorem prover Isabelle/HOL [2], to study these features. Specially, it defines the full static behavior of K a useful sort system for K and suggests several undesirable behaviors in the current K implementations (K 3.6 and K 4.0). To the best of our knowledge, IsaK-Static is the most complete of any existing K specification. We also provide an OCaml based executable full K interpreter generated automatically from the K specification in Isabelle.

Original languageEnglish (US)
Title of host publicationFormal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings
EditorsPeter Csaba Ölveczky, Kyungmin Bae
Number of pages20
ISBN (Print)9783030021450
StatePublished - 2018
Event15th International Conference on Formal Aspects of Component Software, FACS 2018 - Pohang, Korea, Republic of
Duration: Oct 10 2018Oct 12 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11222 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other15th International Conference on Formal Aspects of Component Software, FACS 2018
Country/TerritoryKorea, Republic of

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'IsaK-static: A complete static semantics of K'. Together they form a unique fingerprint.

Cite this