A Complete Semantics of K and Its Translation to Isabelle

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


K [46] 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. Isabelle/HOL [41] is a generic proof engine which allows mathematical formulas to be built into a formal language and provides tools to prove those formulas in a logical calculus. In this paper we define IsaK, a reference semantics for K, which was developed through discussions with the K team to meet their expectations for a semantics for K. Previously, we defined the static semantics for K [28]; thus, this paper mainly focuses on its dynamic semantics. More importantly, we investigate a way to connect K and Isabelle by building a translation framework, TransK, to translate programming languages defined in K into theories defined in Isabelle, which can not only allow programmers to define their programming languages easily in K but also have the ability to reason about their languages in Isabelle. In order to show a well-established translation, we prove that the K specification is sound and relatively complete with respect to the translated Isabelle theory by TransK. To the best of our knowledge, IsaK is the first complete formal semantics defined for K, while TransK is the first complete translation from a real-world, order-sorted algebraic system to a many-sorted one. All the work is formalized in Isabelle/HOL at https://github.com/liyili2/KtoIsabelle.

Original languageEnglish (US)
Title of host publicationTheoretical Aspects of Computing – ICTAC 2021 - 18th International Colloquium, Proceedings
EditorsAntonio Cerone, Peter Csaba Olveczky
Number of pages20
ISBN (Print)9783030853143
StatePublished - 2021
Event18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 - Virtual, Online
Duration: Sep 8 2021Sep 10 2021

Publication series

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


Conference18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021
CityVirtual, Online

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'A Complete Semantics of K and Its Translation to Isabelle'. Together they form a unique fingerprint.

Cite this