LFCS Seminar: Tuesday 11 June - Aleks Boruch⁠-⁠Gruszecki

Title: Capture Tracking

Abstract

Type systems are tools for statically and automatically verifying

properties of programs. Typically types describe the "shapes" of

values: they verify that operations are invoked on appropriate

operands. More sophisticated properties involve inspecting what

operations are invoked, e.g., a function executed during compilation

should not invoke non-deterministic operations such as accessing a

database. Salient topics include effect systems and resource

ownership. These approaches lend themselves to different categories of

properties. We want to verify as many properties as possible, yet

naively integrating different approaches does not yield good results

in practice. Moreover, the industry has been slow to adopt the

aforementioned systems, arguably because the costs of applying them

still outweigh their numerous advantages.

I will present Capture Tracking, an approach which unifies effects and

resources via capabilities tracked in types. Capabilities solve

certain usability problems of effect and resource ownership systems,

particularly in the context of object-oriented programs, and provide a

uniform framework for verifying diverse properties. I will discuss key

motivations for the approach based on the experimental Scala 3

implementation, as well as the foundational Capture Tracking formal

system, CC<:□, together with the key choices behind its design. CC<:□

admits simple and intuitive types for common data structures and their

typical usage patterns, features scoped capabilities which can support

a number of previously studied concepts (incl. algebraic effects), and

was used to guide the implementation.

Links to relevant publications can be found at