Effect systems have been a subject of active research for nearly four decades, with the most notable practical example being checked exceptions in programming languages such as Java. The work on effects can be divided into two strands: The restrictive approach (e.g., Java's checked exceptions) tracks effects that are already built into the language–such as reading and writing state or exceptions–and provides a way to restrict them. The denotational approach, which includes algebraic effects, defines the semantics of computational effects based on primitives. While there are many existing restrictive or denotational effect systems, they are rarely designed with scalability in mind. In this thesis, we design multiple effect systems around the idea of making effect systems scalable when developing large and complex software. The first part of our work is a restrictive path-dependent effect system that provides a granular effect hierarchy by allowing abstract effect members to be bounded. This thesis presents a full formalization of the effect system, and provides an implementation as a part of the Wyvern programming language. The second part of our work presents a denotational effect system that supports abstract algebraic effects. This thesis gives a formalization of the system and provides proofs for type soundness and properties of effect abstraction

93 pages

Thesis Committee:
Jonathan Aldrich (Chair)
Frank Pfenning
Alex Potanin (Victoria Univesity of Wellington)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]