Pith

open record

sign in

arxiv: 1909.01465 · v2 · pith:FI6H6WWB · submitted 2019-09-03 · cs.PL

Towards Gradual Checking of Reference Capabilities

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:FI6H6WWBrecord.jsonopen to challenge →

classification cs.PL
keywords referencecapabilitiesdatagradualcapabilityracesall-inannotated
0
0 comments X
read the original abstract

Concurrent and parallel programming is difficult due to the presence of memory side-effects, which may introduce data races. Type qualifiers, such as reference capabilities, can remove data races by restricting sharing of mutable data. Unfortunately, reference capability languages are an all-in or nothing game, i.e., all the types must be annotated with reference capabilities. In this work in progress, we propose to mix the ideas from the reference capability literature with gradual typing, leading to gradual reference capabilities.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.