Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

La programmation orientée aspect (AOP) vise à améliorer la modularité et la réutilisation des couches logiciels en proposant un mécanisme d’abstraction pour faire face aux préoccupations transversales. Cependant, dans la plupart des langages d’aspects généralistes, les aspects ont un pouvoir presque illimité, rentrant éventuellement en conflit avec ces objectifs. Dans ce travail, nous présentons Effective Aspects : une nouvelle approche pour incorporer le modèle pointcut/advice de l’AOP dans un langage de programmation fonctionnel statiquement typé comme Haskell. Notre travail comprend deux contributions principales. Premièrement, nous définissons un plongement monadique du modèle pointcut/advice complet de l’AOP. La correction du typage est garantie par l’exploitation du système de type sous-jacent, en particulier les types fantômes et une nouvelle classe de type pour faire de l’anti-unification de types. Dans ce modèle, les aspects sont de première classe, peuvent être déployés de façon dynamique, et le langage de pointcuts est extensible, combinant donc la flexibilité des langages d’aspect typés dynamiquement avec les garanties d’un système de type statique. Les monades nous permettent de raisonner directement sur les effets du calcul à la fois dans les aspects et les programmes de base en utilisant des techniques monadiques traditionnelle. Avec ce système, nous étendons la notion de “open modules” avec des effets, et aussi avec les interfaces de pointcut protégés à l’extérieur d’un advice. Ces restrictions sont appliquées statiquement par le système de type. Aussi, nous adaptons les techniques de EffectiveAdvice afin de raisonner sur des propriétés du flot de contrôle. En outre, nous montrons comment contrôler l’interférence des effets en utilisant l’approche fondée sur la paramétricité de EffectiveAdvice. Nous montrons que cette approche n’est pas satisfaisante en présence de multiples aspects et proposons une approche différente en utilisant des vues monadiques, une nouvelle technique pour le traitement de la pile monadique, développée par Schrijvers et Oliveira. Ensuite, nous exploitons les propriétés de notre modèle pour permettre la construction modulaire de nouvelles sémantiques pour la portée d’aspects et le tissage. Notre deuxième contribution s’appuie sur un modèle puissant pour raisonner sur la composition de mixins avec effets et leur interférence, fondée sur un raisonnement équationnelle, paramétrique, et les lois algébriques sur les effets monadiques. Notre contribution est de montrer comment raisonner sur l’interférence en présence de quantification sans restriction pour les pointcuts. Nous montrons que le raisonnement global peut être compositionnelle, ce qui est essentiel pour le passage à l’échelle de l’approche face aux évolutions de grands systèmes. / Aspect-oriented programming (AOP) aims to enhance modularity and reusability in software systems by offering an abstraction mechanism to deal with crosscutting concerns. But, in most general-purpose aspect languages aspects have almost unrestricted power, eventually conflicting with these goals. This work presents Effective Aspects: a novel approach to embed the pointcut/advice model of AOP in a statically-typed functional programming language like Haskell; along two main contributions. First, we define a monadic embedding of the full pointcut/advicemodel of AOP. Type soundness is guaranteed by exploiting the underlying type system, in particular phantom types and a new anti-unification type class. In this model aspects are first-class, can be deployed dynamically, and the pointcut language is extensible, therefore combining the flexibility of dynamically-typed aspect languages with the guarantees of a static type system. Monads enable us to directly reason about computational effects both in aspects and base programs using traditional monadic techniques. Using this we extend the notion of Open Modules with effects, and also with protected pointcut interfaces to external advising. These restrictions are enforced statically using the type system. Also, we adapt the techniques of EffectiveAdvice to reason about and enforce control flow properties as well as to control effect interference. We show that the parametricity-based approach to effect interference falls short in the presence of multiple aspects and propose a different approach using monad views, a novel technique for handling the monad stack, developed by Schrijvers and Oliveira. Then, we exploit the properties of our model to enable the modular construction of new semantics for aspect scoping and weaving. Our second contribution builds upon a powerful model to reason about mixin-based composition of effectful components and their interference, based on equational reasoning, parametricity, and algebraic laws about monadic effects. Our contribution is to show how to reason about interference in the presence of unrestricted quantification through pointcuts. We show that global reasoning can be compositional, which is key for the scalability of the approach in the face of large and evolving systems. We prove a general equivalence theorem that is based on a few conditions that can be established, reused, and adapted separately as the system evolves. The theorem is defined for an abstract monadic AOP model; we illustrate its use with a simple version of the model just described. This work brings type-based reasoning about effects for the first time in the pointcut/advice model, in a framework that is expressive, extensible and well-suited for development of robust aspect-oriented systems as well as a research tool for new aspect semantics.

Ce manuscrit présente une méthode de conception au niveau système reposant sur la programmation fonctionnelle typée et visant à atténuer certains des problèmes complexifiant le développement des systèmes numériques modernes, tels que leurs tailles importantes ou la grande variété des blocs les constituant. Nous proposons un ensemble de mécanismes permettant de mélanger au sein d'un même design plusieurs formalismes de description distincts ("modèles de calcul") se situant potentiellement à des niveaux d'abstraction différents. De plus, nous offrons au concepteur la possibilité d'expliciter directement les paramètres explorables de chaque sous-partie du design, puis d'en déterminer des valeurs acceptables via une étape d'exploration partiellement ou totalement automatisée réalisée à l'échelle du système. Les gains qu'apportent ces stratégies nouvelles sont illustrés sur plusieurs exemples.

Ces travaux s’intéressent à la modélisation formelle de la sémantique des langues naturelles. Pour cela, nous suivons le principe de compositionnalité qui veut que le sens d’une expression complexe soit une fonction du sens de ses parties. Ces fonctions sont généralement formalisées à l’aide du [lambda]-calcul. Cependant, ce principe est remis en cause par certains usages de la langue, comme les pronoms anaphoriques ou les présuppositions. Ceci oblige à soit abandonner la compositionalité, soit modifier les structures du sens. Dans le premier cas, le sens n’est alors plus obtenu par un calcul qui correspond à des fonctions mathématiques, mais par un calcul dépendant du contexte, ce qui le rapproche des langages de programmation qui manipulent leur contexte avec des effets de bord. Dans le deuxième cas, lorsque les structures de sens sont ajustées, les nouveaux sens ont tendance à avoir une structure de monade. Ces dernières sont elles-mêmes largement utilisées en programmation fonctionnelle pour coder des effets de bord, que nous retrouvons à nouveau. Par ailleurs, s’il est souvent possible de proposer le traitement d’un unique phénomène, composer plusieurs traitements s’avère être une tâche complexe. Nos travaux proposent d’utiliser les résultats récents autour des langages de programmation pour parvenir à combiner ces modélisations par les effets de bord. Pour cela, nous étendons le [lambda]-calcul avec une monade qui implémente les effects et les handlers, une technique récente dans l’étude des effets de bord. Dans la première partie de la thèse, nous démontrons les propriétés fondamentales de ce calcul (préservation de type, confluence et terminaison). Dans la seconde partie, nous montrons comment utiliser le calcul pour le traitement de plusieurs phénomènes linguistiques : deixis, quantification, implicature conventionnelle, anaphore et présupposition. Enfin, nous construisons une unique grammaire qui gère ces phénomènes et leurs interactions. / In formal semantics, researchers assign meanings to sentences of a natural language. This work is guided by the principle of compositionality: the meaning of an expression is a function of the meanings of its parts. These functions are often formalized using the [lambda]-calculus. However, there are areas of language which challenge the notion of compositionality, e.g. anaphoric pronouns or presupposition triggers. These force researchers to either abandon compositionality or adjust the structure of meanings. In the first case, meanings are derived by processes that no longer correspond to pure mathematical functions but rather to context-sensitive procedures, much like the functions of a programming language that manipulate their context with side effects. In the second case, when the structure of meanings is adjusted, the new meanings tend to be instances of the same mathematical structure, the monad. Monads themselves being widely used in functional programming to encode side effects, the common theme that emerges in both approaches is the introduction of side effects. Furthermore, different problems in semantics lead to different theories which are challenging to unite. Our thesis claims that by looking at these theories as theories of side effects, we can reuse results from programming language research to combine them.This thesis extends [lambda]-calculus with a monad of computations. The monad implements effects and handlers, a recent technique in the study of programming language side effects. In the first part of the thesis, we prove some of the fundamental properties of this calculus: subject reduction, confluence and termination. Then in the second part, we demonstrate how to use the calculus to implement treatments of several linguistic phenomena: deixis, quantification, conventional implicature, anaphora and presupposition. In the end, we build a grammar that features all of these phenomena and their interactions.

Ce manuscrit présente une méthode de conception au niveau système reposant sur la programmation fonctionnelle typée et visant à atténuer certains des problèmes complexifiant le développement des systèmes numériques modernes, tels que leurs tailles importantes ou la grande variété des blocs les constituant. Nous proposons un ensemble de mécanismes permettant de mélanger au sein d'un même design plusieurs formalismes de description distincts («modèles de calcul») se situant potentiellement à des niveaux d'abstraction différents. De plus, nous offrons au concepteur la possibilité d'expliciter directement les paramètres explorables de chaque sous-partie du design, puis d'en déterminer des valeurs acceptables via une étape d'exploration partiellement ou totalement automatisée réalisée à l'échelle du système. Les gains qu'apportent ces stratégies nouvelles sont illustrés sur plusieurs exemples. / This work presents a novel system-level design method based on typed functional programming and aiming at mitigating some of the issues making the development of modern digital systems complex, such as their increasing sizes and the variety of their subcomponents. We propose a range of mechanisms allowing to mix within a single design several description formalisms (``models of computation''), possibly at different abstraction levels. Moreover, the designer is provided with means to directly express the explorable parameters of each part of their design, and to find acceptable values for them through a partially or totally automatic system-wide architectural exploration step. The advantages brought by those new strategies are illustrated on several examples.