We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Programming Languages

Title: Accelerating Verified-Compiler Development with a Verified Rewriting Engine

Abstract: Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted command-line compiler that is about 1000$\times$ faster while actually featuring simpler compiler-specific proofs.
Comments: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Subjects: Programming Languages (cs.PL)
ACM classes: F.3.1; D.2.4; F.4.2; D.3.4
DOI: 10.4230/LIPIcs.ITP.2022.17
Cite as: arXiv:2205.00862 [cs.PL]
  (or arXiv:2205.00862v3 [cs.PL] for this version)

Submission history

From: Jason Gross [view email]
[v1] Mon, 2 May 2022 12:45:57 GMT (6890kb,D)
[v2] Tue, 12 Jul 2022 17:55:52 GMT (6893kb,D)
[v3] Mon, 18 Jul 2022 17:28:17 GMT (6893kb,D)

Link back to: arXiv, form interface, contact.