A Polymorphic RPC Calculus

TL;DR

This paper introduces a polymorphic RPC calculus enabling flexible multi-tier programming with location polymorphism, and provides a type system and correctness proofs for its translation to monomorphic programs.

Contribution

It extends the RPC calculus with polymorphic location constructs and proves type soundness and correctness of translation to existing monomorphic frameworks.

Findings

Polymorphic RPC calculus supports flexible multi-tier programming.

Type system for polymorphic RPC calculus is sound.

Translation to monomorphic programs is semantically correct.

Abstract

The RPC calculus is a simple semantic foundation for multi-tier programming languages such as Links in which located functions can be written for the client-server model. Subsequently, the typed RPC calculus is designed to capture the location information of functions by types and to drive location type-directed slicing compilations. However, the use of locations is currently limited to monomorphic ones, which is one of the gaps to overcome to put into practice the theory of RPC calculi for client-server model. This paper proposes a polymorphic RPC calculus to allow programmers to write succinct multi-tier programs using polymorphic location constructs. Then the polymorphic multi-tier programs can be automatically translated into programs only containing location constants amenable to the existing slicing compilation methods. We formulate a type system for the polymorphic RPC calculus, and prove its type soundness. Also, we design a monomorphization translation together with proofs on its type and semantic correctness for the translation.