Tue 6 Nov 2018 13:30 - 14:00 at Cabot - 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 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:30 - 15:00
Capabilities and EffectsOCAP at Cabot
13:30
30m
Talk
Designing with Static Capabilities and Effects
OCAP
Colin Gordon Drexel University
14:00
60m
Talk
Formal Methods Panel
OCAP
James Noble Victoria University of Wellington, Philipp Haller KTH, Sweden, Colin Gordon Drexel University