A theory of RPC calculi for client–server model
summary
Extends existing stateless RPC calculi to a stateful calculi family that supports symmetric source-level RPC while implementing asymmetric, trampolined communication for client–server deployments. Introduces a locative type system that statically tracks function locations, removes runtime location checks in sliced client/server code, and enables three strategies: improved stateless state-encoding without runtime checks, a true stateful server strategy that preserves disk/database effects, and a mixed strategy combining both.
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:31Background
- 1:29Introduction
- 3:29The (untyped) RPC calculus
- 5:39The typed RPC calculus
- 9:42The polymorphic RPC calculus
- 10:27Comparison of the RPC calculi
related talks
41mTowards language support for distributed systems
22mLiberating Distributed Consensus
36mDesign Decisions for Communication Systems
37mClassical Processes in modern dress
30mAnatomy of a run-time: your contract with the kernel
12mOn the metatheory of IRs and the CPS-calculus
14mDestination calculus: A linear λ-calculus for purely functional memory writes
32mIntrinsically Typed Sessions with Callbacks