TY - GEN
T1 - K—A semantic framework for programming languages and formal analysis
AU - Chen, Xiaohong
AU - Roşu, Grigore
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2020.
PY - 2020
Y1 - 2020
N2 - We give an overview on the applications and foundations of the $$\mathbb {K}$$ language framework, a semantic framework for programming languages and formal analysis tools. $$\mathbb {K}$$ represents a 20-year effort in pursuing the ideal language framework vision, where programming languages must have formal definitions, and tools for a given language, such as parsers, interpreters, compilers, semantic-based debuggers, state-space explorers, model checkers, deductive program verifiers, etc., can be derived from just one reference formal definition of the language, which is executable, and no other semantics for the same language should be needed. The correctness of the language tools is guaranteed on a case-by-case basis by proof objects, which encode rigorous mathematical proofs as certificates for every individual task that the tools do and can be mechanically checked by third-party proof checkers.
AB - We give an overview on the applications and foundations of the $$\mathbb {K}$$ language framework, a semantic framework for programming languages and formal analysis tools. $$\mathbb {K}$$ represents a 20-year effort in pursuing the ideal language framework vision, where programming languages must have formal definitions, and tools for a given language, such as parsers, interpreters, compilers, semantic-based debuggers, state-space explorers, model checkers, deductive program verifiers, etc., can be derived from just one reference formal definition of the language, which is executable, and no other semantics for the same language should be needed. The correctness of the language tools is guaranteed on a case-by-case basis by proof objects, which encode rigorous mathematical proofs as certificates for every individual task that the tools do and can be mechanically checked by third-party proof checkers.
KW - Formal semantics
KW - K framework
KW - Matching logic
UR - https://www.scopus.com/pages/publications/85089715703
UR - https://www.scopus.com/pages/publications/85089715703#tab=citedBy
U2 - 10.1007/978-3-030-55089-9_4
DO - 10.1007/978-3-030-55089-9_4
M3 - Conference contribution
AN - SCOPUS:85089715703
SN - 9783030550882
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 122
EP - 158
BT - Engineering Trustworthy Software Systems - 5th International School, SETSS 2019, Tutorial Lectures
A2 - Bowen, Jonathan P.
A2 - Liu, Zhiming
A2 - Zhang, Zili
PB - Springer
T2 - 5th International School on Engineering Trustworthy Software Systems, SETSS 2019
Y2 - 21 April 2019 through 27 April 2019
ER -