Type-Safe Dynamic Placement with First-Class Placed Values
summary
A new DSL called Dyno implements placement types with union placement and first-class remote refs, letting the compiler statically track values that may live on cache or DB while still choosing placement at runtime. Formal results include type soundness, placement correctness and architecture conformance; the implementation reimplements an Android app (~7K LOC), finds a real bug, and a survey finds 133 apps use URL-based dynamic placement. Benchmarks show negligible runtime overhead versus RMI.
AI-written summary · about
chapters (8)
- 0:00Type-safe dynamic placement intro
- 2:08Distributed systems challenges
- 3:13Placement types and values
- 5:01Extending with union types
- 8:12Evaluating in real code
- 10:44Antenna Pod case study
- 12:54Performance vs RMI
- 13:36Conclusion and future
related talks
19mExploring Algebraic Placement in Multiparty Languages
11mChoreographic Quick Changes: First-Class Location (Set) Polymorphism
18mRethinking Apps with Local-First Architecture
16mDOGI: Data Placement with Oracle-Guided Insights for Log-Structured Systems
01h 30mImplementing, verifying and debugging distributed event-based systems
33mProgramming Support for Local-First Software
31mFunction-Passing Style Typed, Distributed Functional Programming
45mTaming Distribution: Formal Protocols for Akka Typed