TY - GEN
T1 - Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
AU - Chen, Xiaohong
AU - Lin, Zhengyao
AU - Trinh, Minh Thai
AU - Roşu, Grigore
N1 - Funding Information:
Acknowledgment. The work presented in this paper was supported in part by NSF CNS 16-19275 and an IOHK grant. This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092.
Publisher Copyright:
© 2021, The Author(s).
PY - 2021
Y1 - 2021
N2 - We pursue the vision of an ideal language framework, where programming language designers only need to define the formal syntax and semantics of their languages, and all language tools are automatically generated by the framework. Due to the complexity of such a language framework, it is a big challenge to ensure its trustworthiness and to establish the correctness of the autogenerated language tools. In this paper, we propose an innovative approach based on proof generation. The key idea is to generate proof objects as correctness certificates for each individual task that the language tools conduct, on a case-by-case basis, and use a trustworthy proof checker to check the proof objects. This way, we avoid formally verifying the entire framework, which is practically impossible, and thus can make the language framework both practical and trustworthy. As a first step, we formalize program execution as mathematical proofs and generate their complete proof objects. The experimental result shows that the performance of our proof object generation and proof checking is very promising.
AB - We pursue the vision of an ideal language framework, where programming language designers only need to define the formal syntax and semantics of their languages, and all language tools are automatically generated by the framework. Due to the complexity of such a language framework, it is a big challenge to ensure its trustworthiness and to establish the correctness of the autogenerated language tools. In this paper, we propose an innovative approach based on proof generation. The key idea is to generate proof objects as correctness certificates for each individual task that the language tools conduct, on a case-by-case basis, and use a trustworthy proof checker to check the proof objects. This way, we avoid formally verifying the entire framework, which is practically impossible, and thus can make the language framework both practical and trustworthy. As a first step, we formalize program execution as mathematical proofs and generate their complete proof objects. The experimental result shows that the performance of our proof object generation and proof checking is very promising.
KW - Proof checking
KW - Proof generation
KW - Semantic framework
UR - http://www.scopus.com/inward/record.url?scp=85115834305&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85115834305&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-81688-9_23
DO - 10.1007/978-3-030-81688-9_23
M3 - Conference contribution
AN - SCOPUS:85115834305
SN - 9783030816872
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 477
EP - 499
BT - Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
A2 - Silva, Alexandra
A2 - Leino, K. Rustan
PB - Springer
T2 - 33rd International Conference on Computer Aided Verification, CAV 2021
Y2 - 20 July 2021 through 23 July 2021
ER -