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 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 se fondant sur les travaux de Trimble et al., puis Hughes, on donne une notion de théorie symétrique monoïdale close (smc) et une construction explicite de la catégorie smc engendrée, formant ainsi une adjonction entre théories et catégories. On étudie les exemples du lambda-calcul pur linéaire, du lambda-calcul pur standard, puis des bigraphes de Milner. À chaque fois on donne une théorie smc et on compare la catégorie smc engendrée avec la présentation standard. Entre autres, dans les trois cas, on montre une équivalence entre les deux sur les termes clos. / From the work of Trimble et al. and Hughes, we define a notion of symmetric monoidal closed (smc) theory and give an explicit construction of the smc category generated by it. This construction yields a monadic adjunction between smc theories and smc categories. We study in our algebraic framework different models of programming languages: the linear λ-calculus, the pure λ-calculus and Milner's bigraphs. For each model, we give a smc theory and compare the generated smc category with the standard presentation. We show that, in each case, there is an equivalence on closed terms.