Kappa is a type system for safe concurrent object-oriented programming using reference capabilities. It uses a combination of static and dynamic techniques to guarantee data-race freedom, and, for a certain subset of the system, non-interference (and thereby deterministic parallelism). It combines many features from previous work on alias management, such as substructural types, regions, ownership types, and fractional permissions, and brings them together using a small set of primitives.
In this extended abstract we show how Kappa’s capabilities express variations of the aforementioned concepts, discuss the main insights from working with Kappa, present the current status of the implementation of Kappa in the context of the actor language Encore, and discuss ongoing and future work.
Mon 18 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30
|Are Ownership Types Reaching the World Yet?|
Patrick Lam University of Waterloo, CanadaFile Attached
|Kappa: Insights, Current Status and Future Work|
|Abstract Data Types in Object-Capability Systems|
James Noble Victoria University of Wellington, Sophia Drossopoulou Imperial College London, Mark Miller Google Inc., Toby Murray University of Melbourne, Alex Potanin Victoria University of WellingtonPre-print File Attached