|dc.description.abstract||We present a general semantic account of Gifford-style type-and-effect systems. These
type systems provide lightweight static analyses annotating program phrases with the
sets of possible computational effects they may cause, such as memory access and
modification, exception raising, and non-deterministic choice. The analyses are used,
for example, to justify the program transformations typically used in optimising compilers,
such as code reordering and inlining. Despite their existence for over two
decades, there is no prior comprehensive theory of type-and-effect systems accounting
for their syntax and semantics, and justifying their use in effect-dependent program
We achieve this generality by recourse to the theory of algebraic effects, a development
of Moggi’s monadic theory of computational effects that emphasises the
operations causing the effects at hand and their equational theory. The key observation
is that annotation effects can be identified with the effect operations.
Our first main contribution is the uniform construction of semantic models for typeand-
effect analysis by a process we call conservative restriction. Our construction requires
an algebraic model of the unannotated programming language and a relevant
notion of predicate. It then generates a model for Gifford-style type-and-effect analysis.
This uniform construction subsumes existing ad-hoc models for type-and-effect
systems, and is applicable in all cases in which the semantics can be given via enriched
Our second main contribution is a demonstration that our theory accounts for the
various aspects of Gifford-style effect systems. We begin with a version of Levy’s Callby-
push-value that includes algebraic effects. We add effect annotations, and design
a general type-and-effect system for such call-by-push-value variants. The annotated
language can be thought of as an intermediate representation used for program optimisation.
We relate the unannotated semantics to the conservative restriction semantics,
and establish the soundness of program transformations based on this effect analysis.
We develop and classify a range of validated transformations, generalising many existing
ones and adding some new ones. We also give modularly-checkable sufficient
conditions for the validity of these optimisations.
In the final part of this thesis, we demonstrate our theory by analysing a simple
example language involving global state with multiple regions, exceptions, and nondeterminism.
We give decision procedures for the applicability of the various effect-dependent
transformations, and establish their soundness and completeness.||en
|dc.contributor.sponsor||Scottish Informatics and Computer Science Alliance (SICSA)||en
|dc.contributor.sponsor||Engineering and Physical Sciences Research Council (EPSRC)||en
|dc.publisher||The University of Edinburgh||en
|dc.relation.hasversion||Ohad Kammar, Sam Lindley, and Nicolas Oury, Handlers in action, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (New York, NY, USA), ICFP ’13, ACM, 2013, pp. 145–158.||en
|dc.relation.hasversion||Ohad Kammar and Gordon D. Plotkin, Algebraic foundations for effect-dependent optimisations, Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA), POPL ’12, ACM, 2012, pp. 349–360.||en
|dc.title||Algebraic theory of type-and-effect systems||en
|dc.type||Thesis or Dissertation||en
|dc.type.qualificationname||PhD Doctor of Philosophy||en