Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

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

Permalink

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

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

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

Language

en

Permalink

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

Owning Collections