Designing with Static Capabilities and Effects
Capabilities (whether object or reference capabilities) are fundamentally tools to restrict effects. Thus static capabilities (object or reference) and effect systems take different technical machinery to the same core problem of statically restricting or reasoning about effects in programs. Any time two approaches can in principle address the same sets of problems, it becomes important to understand the trade-offs between the approaches, and how these trade-offs might interact with the problem at hand, and the context of the problem being solved by a given static reasoning approach.
Experts who have worked in these areas tend to find the trade-offs somewhat obvious, having considered them in context before. However, this kind of design discussion is often never written down explicitly in a way that can assist newcomers to the areas. We ourselves have several times set out to solve a problem with one technique, only to find the other better-suited. Other times, our intuition and switch ran the other direction.
We give a concise discussion of the trade-offs between static capabilities (specifically reference capabilities) and effect systems, articulating the types of limitations each approach tends to have in isolation, and how systems of each variety tend to mitigate those issues. We make the discussion concrete by appealing to examples of how these trade-offs were considered in the course of developing prior systems in the area.
Tue 6 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:30 - 15:00 | |||
13:30 30mTalk | Designing with Static Capabilities and Effects OCAP Colin Gordon Drexel University | ||
14:00 60mTalk | Formal Methods Panel OCAP James Noble Victoria University of Wellington, Philipp Haller KTH, Sweden, Colin Gordon Drexel University |