Type Systems for Scope and Effect Safety with Disjointness Reasoning

PhD Qualifying Examination


Title: "Type Systems for Scope and Effect Safety with Disjointness Reasoning"

by

Mr. Cunyuan GAO


Abstract:

Scope safety, effect safety, and disjointness reasoning can protect programs 
from unexpected errors and help compilers improve code performance. Scope 
safety ensures all program entities in a program are well-scoped, i.e., they 
will never be used outside their valid scopes. Effect safety guarantees that 
side effects in programs are correctly encapsulated or handled, avoiding 
runtime errors and indeterministic results in concurrent operations and 
streams. Disjointness reasoning provides the evidence that two elements are 
separated from each other and two operations are non-interfering. Therefore, 
static guarantees for these properties are gaining popularity in recent 
research. Different type systems providing such guarantees usually share 
similar methodologies. This survey investigates the mainstream type systems 
for scope safety, effect safety, and disjointness reasoning, which cover 
effect systems that track effects of expressions, environment classifiers 
that reflect scope relations through abstract quantifiers, contextual modal 
types that integrate types with typing contexts, capability-based approaches 
that restrict programs’ behaviours according to the given capabilities, and 
aliasing control systems that control aliases of objects. One type system 
may rely on one or more technologies to address the problems. We first 
demonstrate the core ideas of these type systems and then propose our novel 
system based on Boolean-Algebraic subtyping and higher-ranked polymorphism.


Date:                   Wednesday, 23 April 2025

Time:                   4:00pm - 6:00pm

Venue:                  Room 2612B
                        Lifts 31/32

Committee Members:      Dr. Lionel Parreaux (Supervisor)
                        Prof. Shing-Chi Cheung (Chairperson)
                        Prof. Charles Zhang