A Polymorphic RPC Calculus

Kwanghoon Choi, James Cheney, Simon Fowler, Sam Lindley

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)
7 Downloads (Pure)


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.
Original languageEnglish
Article number102499
JournalScience of Computer Programming
Early online date5 Jun 2020
Publication statusPublished - 1 Oct 2020


  • multi-tier programming
  • location polymorphism
  • remote procedure call
  • client-server model


Dive into the research topics of 'A Polymorphic RPC Calculus'. Together they form a unique fingerprint.

Cite this