A Typed Slicing Compilation of the Polymorphic RPC Calculus

Kwanghoon Choi, James Cheney, Sam Lindley, Bob Reynders

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.
Original languageEnglish
Title of host publicationProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021)
PublisherACM
Publication statusE-pub ahead of print - 6 Sep 2021
Event23rd International Symposium on Principles and Practice of Declarative Programming - Tallinn, Estonia
Duration: 6 Aug 20218 Aug 2021
https://ppdp2021.github.io/

Symposium

Symposium23rd International Symposium on Principles and Practice of Declarative Programming
Abbreviated titlePPDP 2021
Country/TerritoryEstonia
CityTallinn
Period6/08/218/08/21
Internet address

Keywords

  • multi-tier programming language
  • polymorphism
  • rpc calculus
  • client-server calculus
  • slicing compilation

Fingerprint

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

Cite this