(TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
summary
A compiler for the CP language compiles dynamic inheritance via a merge operator into runtime extensible records with mangled type labels, proving type safety in Coq and targeting JavaScript. The implementation includes coercion elimination and other CP-specific optimizations; benchmarks show optimized CP within about 1.1–2× of handwritten JavaScript on most cases (worst about 3×), and orders-of-magnitude faster than a naive merge compilation. The paper, prototype compiler, benchmarks and Coq formalization are available.
AI-written summary · about
chapters (7)
- 0:00Dynamic inheritance problem
- 1:28Type safety in JavaScript mixing
- 4:23Trait merging for type safety
- 7:39Family polymorphism and expression problem
- 9:05Extensible records compilation
- 12:16Benchmarking performance results
- 13:24Conclusion and future work
related talks
19mExtensible Metatheory Mechanization via Family Polymorphism
37mTCO
21mPolymorphic Type Inference for Dynamic Languages
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
41mThe Dialectics of Type-Level Programming
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
59mCoq to C Translation with Partial Evaluation + Counterexample Generation