TY - GEN
T1 - IsaK-static
T2 - 15th International Conference on Formal Aspects of Component Software, FACS 2018
AU - Li, Liyi
AU - Gunter, Elsa L.
N1 - Funding Information:
Acknowledgements. This material is based upon work supported in part by NSF Grant 0917218. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF.
Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85055083301&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85055083301&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-02146-7_10
DO - 10.1007/978-3-030-02146-7_10
M3 - Conference contribution
AN - SCOPUS:85055083301
SN - 9783030021450
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 196
EP - 215
BT - Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings
A2 - Ölveczky, Peter Csaba
A2 - Bae, Kyungmin
PB - Springer
Y2 - 10 October 2018 through 12 October 2018
ER -