A Typed Slicing Compilation of the Polymorphic RPC Calculus

Kwanghoon Choi; James Cheney; Sam Lindley; Bob Reynders

doi:10.1145/3479394.3479406

A Typed Slicing Compilation of the Polymorphic RPC Calculus

Kwanghoon Choi, James Cheney, Sam Lindley, Bob Reynders

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021)
Publisher	ACM
Number of pages	15
ISBN (Electronic)	978-1-4503-8689-0
DOIs	https://doi.org/10.1145/3479394.3479406
Publication status	Published - 6 Sep 2021
Event	23rd International Symposium on Principles and Practice of Declarative Programming - Tallinn, Estonia Duration: 6 Aug 2021 → 8 Aug 2021 https://ppdp2021.github.io/

Symposium

Symposium	23rd International Symposium on Principles and Practice of Declarative Programming
Abbreviated title	PPDP 2021
Country/Territory	Estonia
City	Tallinn
Period	6/08/21 → 8/08/21
Internet address	https://ppdp2021.github.io/

Keywords

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

Access to Document

10.1145/3479394.3479406Licence: All Rights Reserved

2107.10793v1Accepted author manuscript, 1.04 MBLicence: All Rights Reserved

https://dl.acm.org/doi/10.1145/3479394.3479406Licence: All Rights Reserved

1 Active
2 Finished

Effect Handler Oriented Programming
Lindley, S.
MRC
1/02/21 → 31/01/25
Project: Research
Turing Fellowship
Cheney, J.
UK-based charities
1/09/18 → 31/08/20
Project: Research
Skye-A programming language bridging theory and practice for scientific data curation
Cheney, J.
EU government bodies
1/09/16 → 31/08/22
Project: Research

Cite this

@inproceedings{a5a6c1522c85494f9825db179b81eec9,

title = "A Typed Slicing Compilation of the Polymorphic RPC Calculus",

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. ",

keywords = "multi-tier programming language, polymorphism, rpc calculus, client-server calculus, slicing compilation",

author = "Kwanghoon Choi and James Cheney and Sam Lindley and Bob Reynders",

note = "a long version of ppdp2021; 23rd International Symposium on Principles and Practice of Declarative Programming, PPDP 2021 ; Conference date: 06-08-2021 Through 08-08-2021",

year = "2021",

month = sep,

day = "6",

doi = "10.1145/3479394.3479406",

language = "English",

booktitle = "Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021)",

publisher = "ACM",

url = "https://ppdp2021.github.io/",

}

Choi, K, Cheney, J , Lindley, S & Reynders, B 2021, A Typed Slicing Compilation of the Polymorphic RPC Calculus. in Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021). ACM, 23rd International Symposium on Principles and Practice of Declarative Programming, Tallinn, Estonia, 6/08/21. https://doi.org/10.1145/3479394.3479406

TY - GEN

T1 - A Typed Slicing Compilation of the Polymorphic RPC Calculus

AU - Choi, Kwanghoon

AU - Cheney, James

AU - Lindley, Sam

AU - Reynders, Bob

N1 - a long version of ppdp2021

PY - 2021/9/6

Y1 - 2021/9/6

N2 - 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.

AB - 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.

KW - multi-tier programming language

KW - polymorphism

KW - rpc calculus

KW - client-server calculus

KW - slicing compilation

U2 - 10.1145/3479394.3479406

DO - 10.1145/3479394.3479406

M3 - Conference contribution

BT - Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021)

PB - ACM

T2 - 23rd International Symposium on Principles and Practice of Declarative Programming

Y2 - 6 August 2021 through 8 August 2021

ER -

A Typed Slicing Compilation of the Polymorphic RPC Calculus

Abstract

Symposium

Keywords

Access to Document

Fingerprint

Projects

Effect Handler Oriented Programming

Turing Fellowship

Skye-A programming language bridging theory and practice for scientific data curation

Cite this