English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Compilers are a prime target for formal verification, since compiler bugsinvalidate higher-level correctness guarantees, but compiler changes may becomemore labor-intensive to implement, if they must come with proof patches. Oneappealing approach is to present compilers as sets of algebraic rewrite rules,which a generic engine can apply efficiently. Now each rewrite rule can beproved separately, with no need to revisit past proofs for other parts of thecompiler. We present the first realization of this idea, in the form of aframework for the Coq proof assistant. Our new Coq command takes normal provedtheorems and combines them automatically into fast compilers with proofs. Weapplied our framework to improve the Fiat Cryptography toolchain for generatingcryptographic arithmetic, producing an extracted command-line compiler that isabout 1000$\times$ faster while actually featuring simpler compiler-specificproofs.

Accelerating Verified-Compiler Development with a Verified Rewriting Engine