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 -