Ribbit with Memory Morphisms
summary
Extends Ribbit to synthesize arbitrary morphisms that transform between two concrete memory layouts and to emit CFG-style programs with explicit allocation, casts and destination-passing code; compiles pattern matching into layout-specific decision trees, generates accessors that mask, glue and reassemble split-bit fields (e.g. RISC‑V compressed-instruction bits), and proves the compilation algorithms correct; prototype targets a custom backend (LLVM proved too coarse), includes an online demo, and successfully synthesizes transformations and constructors for recursive types.
AI-written summary · about
chapters (8)
- 0:00Ribbit and memory morphisms
- 5:45Custom memory layouts for ADTs
- 11:52Split-based memory representations
- 17:28Verifying memory layout correctness
- 22:09RISC-V instruction layouts in Ribbit
- 26:49Pattern matching to memory access
- 36:05Contributions and future work
- 37:10Q&A
related talks
32mBit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebr...
31mFormal Specification
01h 05mAll the Languages Together
23mMacro-embedding Compiler Intermediate Languages in Racket
21mWeak Memory Demands Model-based Compiler Testing
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
56mRhombus: The Non-shrubbery Parts (Keynote)
22mGigue: A JIT Code Binary Generator for Hardware Testing