Executing Certified Model Transformations on Apache Spark
summary
A formal refinement of CoqTL produces Parallelizable CoqTL with a mechanized proof of semantic equivalence, then pure Coq functions are manually extracted to Scala and sequential lists are replaced by distributed lists to yield SparkTE on Apache Spark. The pipeline preserves certified contracts (proofs hold on the extracted engine), yields an executable prototype, and on a table→class case study demonstrates clear parallel speedup while relying on Spark’s in‑memory semantics for correctness.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:50Correctness versus scalability
- 3:18CoqTL and SparkTE architecture
- 5:06CoqTL to SparkTE pipeline
- 6:56Transformation workflow
- 15:07Summary
related talks
30mFormal verification of Scala programs with Stainless
28mUpgrade Tooling w/Spark: It's not just for language versions
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
38mGenerative Programming and Verification
32mSafer Code with LLMs: Scala Types Silver Bullet?
47mScala: The Unpredicted Lingua Franca for Data Science
47mScala: The Unpredicted Lingua Franca for Data Science
45mFuture proofing Scala the TASTY intermediate rep