Relational Compilation for Performance-Critical Applications
summary
Claims a proof-producing toolkit (Rupicola) that compiles specific high-level functional programs into low-level imperative code by proving "there exists" target code in Coq, then emits Bedrock2/C. It implements relational compilation with automated loop-invariant inference and mutation introduction without monads, packs proofs checked by the Coq kernel, and benchmarks small string/network/data-structure kernels where generated C is often indistinguishable from handwritten C (performance parity reported on most microbenchmarks). Output is correct but currently not human-readable.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:03High-level vs low-level
- 3:46Functional programs inefficiency
- 6:10Rupicola toolkit
- 7:33Relational compilation in Rupicola
- 9:40Compiling string uppercasing
- 11:47Rupicola innovations
- 12:50Benchmarks and case studies
- 15:37Summary
- 16:38Q&A
related talks
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
19mCertified Compilers à la Carte
23mTowards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
29mTowards Formally Verified Just-In-Time Compilation
16mMulti-stage Relational Programming
58mFast Cryptographic Code via Partial Evaluation
15mCompiling with Continuations, Correctly