University of Illinois Urbana-Champaign

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

Xiaohong Chen; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu

Content Files
chen-lin-trinh-rosu-2021-tr.pdf

Permalink

https://hdl.handle.net/2142/109927

Description

Title
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
Author(s)
  • Xiaohong Chen
  • Zhengyao Lin
  • Minh-Thai Trinh
  • Grigore Rosu
Issue Date
2021-04
Keyword(s)
  • Semantic framework
  • Proof generation
  • Proof checking
Date of Ingest
2021-05-01T02:48:18Z
Abstract
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.
Type of Resource
text
Genre of Resource
technical report
Language
en
Permalink
http://hdl.handle.net/2142/109927

Owning Collections

Research and Tech Reports - Computer Science PRIMARY