DimSum: A Decentralized Approach to Multi-language Semantics and Verification

on YouTube ↗25m

" summary

DimSum presents a decentralized method that avoids fixing a source language, memory model, or closed set of languages by giving each language a labeled-transition module semantics and composing them with semantic wrappers and combinators. The framework is implemented in Coq and instantiated for three languages: Rec, Asm, Spec. The paper verifies an optimizing multi-pass compiler Rec→Asm and two case studies: an Asm pointer-comparison library and an Asm coroutine library, showing Asm code can be abstracted to Rec-level specs.

AI-written summary · about

" chapters (10)

1. 0:00Introduction
2. 0:35The challenge of multi-language
3. 4:00Existing approaches and limitations
4. 6:23Introducing Dim Sum
5. 8:48Defining refinement in Dim Sum
6. 11:08Semantic linking
7. 13:27Wrappers and translation
8. 15:36Verification in practice
9. 19:40Conclusion and recap
10. 20:52Q&A session