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.
Conference DayMon 18 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30
|Are Ownership Types Reaching the World Yet?|
Patrick LamUniversity of Waterloo, CanadaFile Attached
|Kappa: Insights, Current Status and Future Work|
|Abstract Data Types in Object-Capability Systems|
James NobleVictoria University of Wellington, Sophia DrossopoulouImperial College London, Mark MillerGoogle Inc., Toby MurrayUniversity of Melbourne, Alex PotaninVictoria University of WellingtonPre-print File Attached