TY - GEN

T1 - A Complete Semantics of K and Its Translation to Isabelle

AU - Li, Liyi

AU - Gunter, Elsa L.

N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85115199410&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85115199410&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-85315-0_10

DO - 10.1007/978-3-030-85315-0_10

M3 - Conference contribution

AN - SCOPUS:85115199410

SN - 9783030853143

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 152

EP - 171

BT - Theoretical Aspects of Computing – ICTAC 2021 - 18th International Colloquium, Proceedings

A2 - Cerone, Antonio

A2 - Olveczky, Peter Csaba

PB - Springer

T2 - 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021

Y2 - 8 September 2021 through 10 September 2021

ER -