IsaK-static: A complete static semantics of K

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

Abstract

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
PublisherSpringer-Verlag Berlin Heidelberg
Pages196-215
Number of pages20
ISBN (Print)9783030021450
DOIs
StatePublished - Jan 1 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

Other

Other15th International Conference on Formal Aspects of Component Software, FACS 2018
CountryKorea, Republic of
CityPohang
Period10/10/1810/12/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Li, L., & Gunter, E. L. (2018). IsaK-static: A complete static semantics of K. In P. C. Ölveczky, & K. Bae (Eds.), Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings (pp. 196-215). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11222 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-030-02146-7_10