Leveraging DSLs (Almost) for Free
summary
A method called verified lifting automatically infers a high‑level spec from code, proves equivalence with a theorem prover, and generates DSL code; a framework called Metalift plus a concrete compiler Casper produce production artifacts and are open source. Experiments translate Java→SQL, Fortran→CUDA/Halide, Java→Spark/Hadoop, converting 50 of 60 collected benchmarks, median compile time under five minutes, and deliver up to 31x speedup (20x reported for GPU cases).
AI-written summary · about
chapters (6)
- 0:00Start
- 9:36Program Compilation vs. Synthesis
- 20:48Casper Architecture
- 26:11Performance: Is Casper competitive?
- 28:20Performance Analysis: Is Casper Practical?
- 33:12Verified lifting using program synthesis for code translation
related talks
26mAI-powered Productivity using Open-Source LLMs
26mSame API, Different Execution
28mA community based open source LLM and what it can do for your business
42mOpen Source LLMs — Powering AI Accessibility and Innovation
17mComposable Data Management Systems
01h 16mHow Will LLMs Change Haskell, Programming and Open Source?
22mOpen source design testing and verification with UVM and Verilator
45mEnable Digital Sovereignty by Tech Stack Liquidity