TY - CHAP
T1 - The K Vision for the Future of Programming Language Design and Analysis
AU - Chen, Xiaohong
AU - Roşu, Grigore
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - Formal programming language semantics should be a unique opportunity to give birth to a better language, not a cumbersome post-mortem activity. Moreover, language implementations and analysis tools should be automatically generated from the formal semantics in a correct-by-construction manner, at no additional cost. In this paper, we discuss how we are pursuing this vision of programming language design and analysis within the context of the K framework (http://kframework.org ), where it is easy and fun to design and deploy new programming languages; where language designers can focus on the desired features and not worry about their implementation; and where the correctness of all auto-generated language implementations and tools is guaranteed on a case-by-case basis, and every individual task, be it parsing, execution, verification, or anything else, is endorsed by its own proof object that can be independently checked by third-party proof checkers, making no compromise to safety or correctness.
AB - Formal programming language semantics should be a unique opportunity to give birth to a better language, not a cumbersome post-mortem activity. Moreover, language implementations and analysis tools should be automatically generated from the formal semantics in a correct-by-construction manner, at no additional cost. In this paper, we discuss how we are pursuing this vision of programming language design and analysis within the context of the K framework (http://kframework.org ), where it is easy and fun to design and deploy new programming languages; where language designers can focus on the desired features and not worry about their implementation; and where the correctness of all auto-generated language implementations and tools is guaranteed on a case-by-case basis, and every individual task, be it parsing, execution, verification, or anything else, is endorsed by its own proof object that can be independently checked by third-party proof checkers, making no compromise to safety or correctness.
KW - K framework
KW - Language frameworks
KW - Programming language design
UR - http://www.scopus.com/inward/record.url?scp=85117533613&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85117533613&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-87348-6_1
DO - 10.1007/978-3-030-87348-6_1
M3 - Chapter
AN - SCOPUS:85117533613
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 9
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PB - Springer
ER -