A Theory of RPC Calculi for Client-Server Model

TL;DR

This paper introduces a typed RPC calculus that tracks client and server locations at the type level, providing a formal foundation for multi-tier programming languages in web development.

Contribution

It proposes a novel located type system for RPC calculi, enabling formal reasoning about client-server interactions with static location tracking.

Findings

Developed a typed RPC calculus with location-aware types

Laid theoretical groundwork for multi-tier web programming languages

Enhanced with polymorphic locations and slicing compilation in subsequent work

Abstract

With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client-server model where programmers write client and server programs separately and test the multiple programs together. The RPC calculus, one of the foundations of those languages by Cooper and Wadler, has the feature of symmetric communication in programmer's writing arbitrarily deep nested client-server interactions. However, the existing research only considers dynamically typed locations. We propose a typed RPC calculus where locations are tracked in type-level. A new located type system paves the way for a theory of RPC calculi for the client-server model. (In the following papers published in SCP2020 and PPDP2021, the typed RPC calculus will be enhanced with polymorphic locations and a type-based slicing compilation.)