Show simple item record

dc.contributor.advisorPlotkin, Gordonen
dc.contributor.advisorSimpson, Alexen
dc.contributor.authorKammar, Ohaden
dc.date.accessioned2014-06-03T12:50:52Z
dc.date.available2014-06-03T12:50:52Z
dc.date.issued2014-06-27
dc.identifier.urihttp://hdl.handle.net/1842/8910
dc.description.abstractWe 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 transformation. 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 Lawvere theories. 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.sponsorScottish Informatics and Computer Science Alliance (SICSA)en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoen
dc.publisherThe University of Edinburghen
dc.relation.hasversionOhad 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.hasversionOhad 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.subjectprogramming languageen
dc.subjectdenotational semanticsen
dc.subjecttype-and-effect systemsen
dc.subjectLawvere theoriesen
dc.subjectmonadsen
dc.titleAlgebraic theory of type-and-effect systemsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record