Nouvelles fonctions dans les interfaces de communication pour l'augmentation des performances réseau des machines multi-processeur.

  • By: Eric Lemoine
  • Number: PhD2004-01
  • Date: Juillet 2004
  • Abstract:

    Today's networks are improving faster than uniprocessor technology, making it increasingly difficult for a single processor to keep up with a high-speed network. With multiprocessor machines becoming commodities, and with the emergence of multithreaded processors, applying multiple execution units to high-speed networks represents an interesting opportunity. This thesis proposes new functionality in the network controller --- the classification of incoming packets and of transmission notifications --- in order to intelligently distribute network processing across processors, and thereby maximize the execution efficiency of the operating system's communication software. Software prototypes have been developed on programmable network controllers. The experimental results, presented and analyzed in this thesis, demonstrate the relevance of the proposed solutions.
  • Abstract (in french):

    Les progrès dans le domaine des réseaux informatiques semblent aujourd'hui plus rapides que ceux dans le domaine des processeurs à flot d'exécution unique. Il devient ainsi de plus en plus difficile pour un processeur de soutenir le débit du réseau. Avec la démocratisation des technologies multi-processeur et l'émergence des processeurs multi-flot (processeurs multi-threadés), l'utilisation simultanée de plusieurs unités d'exécution pour les traitements relatifs au réseau constitue une opportunité intéressante pour faire face aux hauts débits des réseaux. Dans ce contexte, cette thèse propose des nouvelles fonctions dans les contrôleurs réseau --- la classification des paquets entrants et le tri des notifications d'émission --- dans l'optique de répartir intelligemment les traitements réseau parmi les processeurs et ainsi de maximiser l'efficacité des logiciels de communication dans le système d'exploitation. Des prototypes logiciels ont été développés sur des contrôleurs réseau programmables. Les résultats des expériences réalisées, présentés et analysés dans la thèse, démontrent la pertinence des solutions proposées.
  • Keywords:

    Networking, performance, multi-processor, networking system, parallelism, network interface controller, server, operating system.
    Keywords (in french):

    Réseau, performance, multi-processeur, système de communication, parallélisme, contrôleur réseau, serveur, système d'exploitation.
  • Availability: Electronic copy only.
  • Size: 129p
  • Format: pdf
  • Get it

Étude et optimisation du comportement mémoire dans les méthodes parallèles de factorisation de matrices creuses.

  • By: Abdou Guermouche
  • Number: PhD2004-02
  • Date: Juillet 2004
  • Abstract:

    Direct methods for solving sparse linear systems are known for their large memory requirements that can represent the limiting factor to solve large systems. The work done during this thesis concerns the study and the optimization of the memory behaviour of a sparse direct method, the multifrontal method, for both the sequential and the parallel cases. Thus, optimal memory minimization algorithms have been proposed for the sequential case. Concerning the parallel case, we have introduced new scheduling strategies aiming at improving the memory behaviour of the method. After that, we extended these approaches to have a good performance while keeping a good memory behaviour. In addition, in the case where the data to be treated cannot fit into memory, out-of-core factorization schemes have to be designed. To be efficient, such approaches require to overlap I/O operations with computations and to reuse the data sets already in memory to reduce the amount of I/O operations. Therefore, another part of the work presented in this thesis concerns the design and the study of implicit out-of-core techniques well-adapted to the memory access pattern of the multifrontal method. These techniques are based on a modification of the standard paging policies of the operating system using a low-level tool (MMUM&MMUSSEL).
  • Abstract (in french):

    Les méthodes directes de résolution de systèmes linéaires creux sont connues pour leurs besoins mémoire importants qui peuvent constituer une barrière au traitement de problèmes de grandes taille. De ce fait, les travaux effectués durant cette thèse ont porté d'une part sur l'étude du comportement mémoire d'un algorithme de factorisation de matrices creuses, en l'occurrence la méthode multifrontale, et d'autre part sur l'optimisation et la minimisation de la mémoire nécessaire au bon déroulement de la factorisation aussi bien dans un cadre séquentiel que parallèle. Ainsi, des algorithmes optimaux pour la minimisation de la mémoire ont été proposés pour le cas séquentiel. Pour le cas parallèle, nous avons introduit dans un premier temps des stratégies d'ordonnancement visant une amélioration du comportement mémoire de la méthode. Puis, nous les avons étendues pour avoir un objectif de performance tout en gardant un bon comportement mémoire. Enfin, dans le cas où l'ensemble des données à traiter a encore une taille plus importante que celle de la mémoire, il est nécessaire de concevoir des approches de factorisation out-of-core. Pour être efficaces, ces méthodes nécessitent d'une part de recouvrir les opérations d'entrées/sorties par des calculs, et d'autre part de réutiliser des données déjà présentes en mémoire pour réduire le volume d'entrées/sorties. Ainsi, une partie des travaux présentés dans cette thèse ont porté sur la conception de techniques out-of-core implicites adaptées au schéma des accès de la méthode multifrontale et reposant sur une modification de la politique de pagination du système d'exploitation à l'aide d'un outil bas-niveau (MMUM&MMUSSEL).
  • Keywords:

    Sparse matrices, multifrontal method, reordering techniques, memory, scheduling, paging.
    Keywords (in french):

    Matrices creuses, méthodes multifrontale, techniques de renumérotation, mémoire, ordonnancement, pagination.
  • Availability: Electronic copy only.
  • Size: 174p
  • Format: pdf
  • Get it

Expressivite des logiques d'espace.

  • By: Etienne Lozes
  • Number: PhD2004-03
  • Date: Novembre 2004
  • Abstract:

    Spatial logics are a new formalism for specifying properties of concurrent systems in the line of modal logics (Hennessy - Milner). They may be seen also as an extension of classical logic better suited for giving an axiomatic semantics for imperative programs manipulating pointers in the line of Hoare-Floyd logic. This thesis present these several issues and compare the different approaches from the point of view of expressiveness. Several encoding, minimal fragments, and decidability results are presented.
  • Abstract (in french):

    Les logiques spatiales sont une nouvelle classe de formalismes dedies a la specification des systemes distribues dans la lignee des logiques modales (Hennessy-Milner). Elles peuvent aussi etre vues comme une extension de la logique classique mieux adaptee a la semantique axiomatique des langages imperatifs manipulant des pointeurs, dans la lignee de la logique de Hoare-Floyd. Cette these presente ces diverses logiques en les comparant du point de vue de leur expressivite. On etablit ainsi des encodages des logiques, des fragments minimaux, des unifications de logiques, et des resultats de decidabilite.
  • Keywords:

    Spatial logics, concurrency, Hoare logic, expressiveness, decidability.
    Keywords (in french):

    Logiques spatiales, concurrence, logique de Hoare, expressivite, decidabilite.
  • Availability: Electronic copy only.
  • Size: 239p
  • Format: postscript compressed
  • Get it

Ressources limitées pour la mobilité : utilisation, réutilisation, garanties.

  • By: David Teller
  • Number: PhD2004-04
  • Date: Novembre 2004
  • Abstract:

    Whether it is a cell phone or a web server, an applet or a network packet, any software or hardware system is constrained by limitations on resources. Some have limited access to memory, others to disk or network connections. In particular, it is necessary to control the allocation and deallocation of resources, as well as the respect of protocols, so as to prevent overflows, attacks or misuse. Although this aspect of mobile and communicating systems is crucial, it is currently ignored by most process algebras. In order to address this problem, we have studied the notion of resources and formalized it, in calculi based on site mobility (i.e. Mobile Ambients) or name mobility (i.e. pi-calculus). We thus uncovered mechanisms for allocation and deallocation and methods to permit reuse of resources. Furthermore, we designed type systems to guarantee statically that a system, when executed, will never require more resources than it is allowed to use.
  • Abstract (in french):

    Qu'il s'agisse de téléphones portables ou de serveurs web, d'applets ou de paquets réseau, les systèmes matériels et logiciels sont contraints par des limitations sur les ressources telles que la mémoire, l'utilisation du disque ou les connexions au réseau. En particulier, il est nécessaire de contrôler l'allocation et la désallocation des ressources ainsi que le respect de protocoles, afin de prévenir les dépassements de capacité ou d'autres formes d'attaque ou d'accidents. Ce aspect, pourtant central dans la conception d'applications mobiles et communicantes, est ignoré par la majorité des algèbres de processus. Afin de contribuer à résoudre ce problème, nous avons étudié la notion de ressources. Nous avons formalisé cette notion dans le contexte de calculs conçus autour de la mobilité de sites, tels que les Mobile Ambients, ou de la mobilité de noms, comme le pi-calcul. Nous avons ainsi mis en évidence les mécanismes d'allocation et de désallocation de ressources et dégagé des méthodes pour prendre en compte les ressources et de les réutiliser intelligemment. De plus, les systèmes de types que nous avons conçus permettent de garantir statiquement qu'un système, au cours de son exécution, ne nécessitera pas plus de ressources qu'il n'est autorisé à en utiliser.
  • Keywords:

    Resources, mobility, distribution, concurrency, process algebras, type systems, protocols, memory.
    Keywords (in french):

    Ressources, mobilité, distribution, parallélisme, algèbres de processus, systèmes de types, protocoles, mémoire.
  • Availability: Electronic copy only.
  • Size: 284p
  • Format: postscript compressed
  • Get it

Preuves formelles en arithmétiques à virgule flottante.

  • By: Sylvie Boldo
  • Number: PhD2004-05
  • Date: Novembre 2004
  • Abstract:

    This work is representative of my experiments on joining computer arithmetic, directed by the IEEE-754 standard, and formal proofs, here the Coq proof assistant. The floating-point number formalization used was first developed by L. Théry. I first tested and expanded the library with properties that are easy to express in our formalism: the fact that a real value may be represented exactly by a floating-point number. I then tried some extensions of the model: bring it closer to the hardware realities, generalize it to use the two's complement representation and go into a weaker rounding. With these results, I studied two applications. The first one is a multi-precision library using expansions. The second one is the evaluation of elementary functions (logarithm, cosine...): I solved the main problems of argument reduction by formally proving the conditions and algorithms involved and I studied the polynomial evaluation using Horner's rule. I showed the possibility to make formal proofs about the difficult topic of computer arithmetic. I found the advantages and drawbacks of this method by getting enough distance from the formalization by three different means: supplements to the library, extensions of the formalization and validation of real-life applications.
  • Abstract (in french):

    Cette thèse est représentative de mon expérience de rapprochement de l'arithmétique à virgule flottante, régie par la norme IEEE-754, et de la preuve formelle, ici l'assistant de preuves Coq. La formalisation des nombres flottants utilisée a été premièrement développée par L. Théry. J'ai tout d'abord testé et enrichi la bibliothèque avec des propriétés simples à exprimer dans le formalisme choisi: le fait qu'une valeur réelle soit exactement représentable par un nombre flottant. J'ai ensuite fait différentes extensions du modèle: rapprochement avec la réalité matérielle des processeurs, généralisation à la représentation en complément à 2 et étude d'un arrondi plus faible. En utilisant les résultats précédents, j'ai étudié deux applications réelles. La première est une bibliothèque de calcul multi-précision basée sur les expansions. La seconde est l'évaluation de fonctions élémentaires (exponentielle, cosinus...): j'ai résolu la plupart des problèmes de la réduction d'argument en garantissant formellement les conditions et algorithmes associés et j'ai étudié l'évaluation polynomiale par l'algorithme de Horner. J'ai montré la faisabilité de preuves formelles dans le domaine complexe de l'arithmétique des ordinateurs. J'ai déterminé les points forts et les limites de cette démarche en obtenant un recul suffisant face à cette formalisation par différents moyens: enrichissement de la bibliothèque, extensions du modèle et validation de vraies applications.
  • Keywords:

    Computer arithmetic, Floating-point numbers, Formal proof, Coq.
    Keywords (in french):

    Arithmétique des ordinateurs, Nombres à virgule flottante, Preuve formelle, Coq.
  • Availability: Electronic copy only.
  • Size: 146p
  • Format: pdf
  • Get it

Aspects combinatoires des pavages.

  • By: Frédéric Chavanon
  • Number: PhD2004-06
  • Date: Décembre 2004
  • Abstract:

    In the context of studying sets of tilings, we focus on the case of tilings of zonotopes (which are figures of a space defined by all linear combinations of a given set of vectors). We first define a graph which is a dual of a tiling of a planar zonotope using the adjacency relation between tiles, then we prove the one-to-one correspondence between the two sets. We also study how the flip operation (which is a local reorganization of tiles) is defined on the dual, allowing to study the set of tilings of the corresponding zonotope. This method can only hardly apply to higher dimensional cases (non planar zonotopes), we finalized a method by decomposition allowing to study a tiling by considering the properties of smaller tilings. This kind of method was performed to prove strong results on the reconstruction and structure of tilings in the particular case of codimension 2. Moreover, this allowed to show a connectivity result on some cases of high dimension. We chose zonotopal tilings for they extend quite naturally some classically studied tilings (such as domino tilings on the square lattice or lozenge tilings on the triangular lattice). Moreover, these tilings are not defined on a lattice, and they are defined for any dimension.
  • Abstract (in french):

    Dans le cadre de l'étude des ensembles de pavages, nous nous sommes concentrés sur le cas des pavages de zonotopes (figures d'un espace formées de toutes les combinaisons linéaires d'un ensemble de vecteurs donnés). Après avoir défini un graphe dual d'un pavage de zonotope planaire (par l'utilisation de la relation d'adjacence liant les tuiles), nous avons montré la relation biunivoque qui lie les deux classes d'objets. Nous avons alors étudié comment l'opération de flip (qui est un réarrangement local de tuiles) peut s'exprimer sur le dual, permettant par la suite de construire l'ensemble des pavages du zonotope associé. Cette méthode ne pouvant que très difficilement s'adapter aux cas de dimensions supérieures (zonotopes non planaires), nous avons alors mis au point une méthode de décomposition permettant d'étudier un pavage en nous focalisant sur les propriétés de pavages plus petits. Ce type de méthode nous a permis de démontrer des résultats forts de reconstruction et de structure dans le cas de pavages de dimension 2. De plus, ceci nous a permis de démontrer des résultats de connexité dans certains cas particuliers de dimensions supérieures. Le choix des pavages de zonotopes étend naturellement certains pavages étudiés classiquement (tels que les pavages de dominos sur une grille carrée ou de losanges sur une grille triangulaire). En effet, ils ne peuvent être définis sur une grille, et sont définis en toute dimension.
  • Keywords:

    Tilings, Algorithms, Combinatorics, Order theory.
    Keywords (in french):

    Pavages, Algorithmique, Combinatoire, Théorie des ordres.
  • Availability: Electronic copy only.
  • Size: 104p
  • Format: pdf
  • Get it

Robustesse de la dynamique des systèmes discrets : le cas de l'asynchronisme dans les automates cellulaires.

  • By: Nazim Fates
  • Number: PhD2004-07
  • Date: Décembre 2004
  • Abstract:

    The aim of this work is to study what happens when the dynamics of a cellular automaton is perturbed (for example when the transitions are not all made at each time step). We give a formal framework to the informal concept of ``robusteness'' in order to explain why some cellular automata keep their behaviour constant while others change their behaviour, either in a continuous way, or with ``phase transitions''. The main question thus consists in quantifying the phenomena using appropriate measures. We propose a method of classification of cellular automata that use the statistical variations of the density parameter. Starting from these results, the robustnes of various automata is estimated experimentally. Results show that the celular automata studided can indeed be partionned in to various classes. Some of these classes are then studied analytically with probabilistic models such as martingales and Markov chains. Other automata are studied experimentally : we give evidence that some of the transition phases belong to the universality class and we study how the robustness of the Game of Life evolves with topology perturbations.
  • Abstract (in french):

    L'objet de ce travail est d'étudier ce qui se produit lorsque l'on perturbe la dynamique d'un automate cellulaire (par exemple en n'effectuant plus toutes les transitions de façon synchrone). Notre motivation est de parvenir à donner un cadre formel qui puisse décrire la notion informelle de ``robustesse'' : on constate que certains automates cellulaires gardent ``le même type de comportement'' lorsqu'ils sont perturbés alors que d'autres automates changent leur comportement soit de façon continue, soit de façon ``brutale'' (on parle alors de transition de phase). La question principale consiste donc à quantifier les phénomènes observés en utilisant les mesures appropriées. Nous proposons une méthode de classification des automates cellulaires qui utilise les variations statistiques du paramètre densité. Partant de ces premiers résultats, nous étudions la notion de robustesse à l'asynchronisme selon un protocole expérimental similaire. Ces études permettent de effectivement de classer les automates en des classes distinctes ; certaines d'entre elles sont en partie étudiées analytiquement à l'aide de modèles probabilistes (martingales et chaines de Markov) qui permettent d'estimer les temps de convergence vers un point fixe. D'autres automates sont étudiés expérimentalement : nous montrons en particulier l'existence de transitions de phase appartenant à la classe d'universalité de la percolation dirigée et nous examinons la robustesse du Jeu de la Vie à la lumière de modifications de topologie.
  • Keywords:

    synchronous cellular automata, discrete dynamical systems, stochastic process, phase transitions.
    Keywords (in french):

    automates cellulaires asynchrones, systèmes dynamiques discrets, processus stochastiques, transitions de phase.
  • Availability: Electronic copy only.
  • Size: 180p
  • Format: pdf
  • Get it

Décomposition algorithmique des graphes.

  • By: Frederic Mazoit
  • Number: PhD2004-08
  • Date: Décembre 2004
  • Abstract:

    In this thesis, we study two graph decompositions introduced by Roberston and Seymour: the tree-decompositions and the branch-decompositions. Two graph parameters are associated to these decompositions: the treewidth and the branchwidth. We show how these decompositions can be united under a common combinatorial structure; both treewidth and branchwidth correspond to minimal values of parameters on this common structure. Using this parallel we adapt a general algorithm that computes the treewidth of some graphs to the branchwidth. We can apply this new algorithm to graphs of bounded asteroidal number with polynomial number of minimal separators and d-trapezoid circular graphs. We also use this analogy to adapt structural properties of branch-decompositions to tree-decompositions. In the case of planar graphs, we give a topological interpretation of these properties which leads us to a simple proof of a theorem linking the treewidth of a planar graph to the treewidth of its dual. Using this topological point of view, we also give an efficient algorithm to list the minimal separators of a planar graph.
  • Abstract (in french):

    Dans cette thèse, nous nous intéressons à deux types de décompositions des graphes introduits par Robertson et Seymour: les décompositions arborescentes et les décompositions en branches. À ces décompositions sont associés deux paramètres des graphes: la largeur arborescente et la largeur de branches. Nous montrons que ces deux décompositions peuvent être vues comme issues d'une même structure combinatoire; les deux paramètres mentionné ci-dessus sont égaux aux valeurs minimales de deux paramètres de cette structure commune. En poussant plus avant cette analogie, nous montrons comment adapter une technique de calcul de la largeur arborescente au calcul de la largeur de branches. Ceci nous permet de calculer la largeur de branches des graphes de nombre astéroïde borné ayant un nombre polynômial de séparateurs minimaux et celle des graphes d-trapézoïdes circulaires. Ce parallèle nous permet aussi d'adapter certains résultats structurels sur les décompositions en branches aux décompositions arborescentes. Dans le cas des graphes planaires, nous interprétons ces propriétés à l'aide d'outils topologiques. De cette façon, nous donnons une démonstration simple d'un théorème de dualité reliant la largeur arborescente d'un graphe planaire et celle de son dual. Ces outils nous permettent aussi d'énumérer de façon efficace les séparateurs minimaux des graphes planaires.
  • Keywords:

    raphs, hyper-graphs, tree-decomposition, branch decompositions, matriochkas, exact calculus, circular-arc graphs, graphs of bounded asteroïdal number with a polynomial number of minimal separators, planar hyper-graphs, duality.
    Keywords (in french):

    graphes, hyper-graphes, décomposition arborescentes, décomposition en branches, matriochkas, calcul exact, graphes d'intervalles circulaires, graphes de nombres astéroïdes borné ayant un nombre polynomial de séparateur minimal, hyper-graphes planaires, dualité.
  • Availability: Electronic copy only.
  • Size: 150p
  • Format: pdf
  • Get it

Arithmétique et algorithmique en algèbre linéaire exacte pour la bibliothèque LinBox.

  • By: Pascal Giorgi
  • Number: PhD2004-09
  • Date: Décembre 2004
  • Abstract:

    For a few decades, numerical linear algebra has seen intensive developments in both mathematical and computer science theory which have led to genuine standard software like BLAS or LAPACK. In computer algebra the situation has not advanced as much, in particular because of the diversity of the problems and because of much of the theoretical progress have been done recently. This thesis falls into a recent class of work which aims at uniforming high-performance codes from many specialized libraries into a single platform of computation. In particular, the emergence of robust and portable libraries like GMP or NTL for exact computation has turned out to be a real asset for the development of applications in exact linear algebra. In this thesis, we study the feasibility and the relevance of the re-use of specialized codes to develop a high performance exact linear algebra library, namely the LinBox library. We use the generic programming mechanisms of C++ (abstract class, template class) to provide an abstraction of the mathematical objects and thus to allow the plugin of external components. Our objective is then to design and validate, in LinBox, high level generic toolboxes for the implementation of algorithms in exact linear algebra. In particular, we propose "exact/numeric" hybrid computation routines for dense matrices over finite fields which nearly match with the performance obtained by numerical libraries like LAPACK. On a higher level, we reuse these hybrid routines to solve very efficiently a classical problem of computer algebra: solving diophantine linear systems. Hence, this allowed us to validate the principle of code reuse in LinBox library and more generally in computer algebra. The LinBox library is available at www.linalg.org ..
  • Abstract (in french):

    L'algèbre linéaire numérique a connu depuis quelques décennies des développements intensifs autant au niveau mathématique qu'informatique qui ont permis d'aboutir à de véritable standard logiciel comme BLAS ou LAPACK. Dans le cadre du calcul exact ou formel, la situation n'est pas aussi avancée, en particulier à cause de la diversité des problématiques et de la jeunesse des progrès théoriques. Cette thèse s'inscrit dans une tendance récente qui vise à fédérer des codes performants provenant de bibliothèques spécialisées au sein d'une unique plateforme de calcul. En particulier, l'émergence de bibliothèques robustes et portables comme GMP ou NTL pour le calcul exact s'avére être un réel atout pour le développement d'applications en algèbre linéaire exacte. Dans cette thèse, nous étudions la faisabilité et la pertinence de la réutilisation de codes spécialisés pour développer une bibliothèque d'algèbre linéaire exacte performante, à savoir la bibliothèque LinBox. Nous nous appuyons sur les mécanismes C++ de programmation générique (classes abtraites, classes templates) pour fournir une abstraction des composantes mathématiques et ainsi permettre le plugin de composants externes. Notre objectif est alors de concevoir et de valider des boîtes à outils génériques haut niveau dans LinBox pour l'implantation d'algorithmes en algèbre linéaire exacte. En particulier, nous proposons des routines de calcul hybride "exact/numérique" pour des matrices denses sur un corps finis permettant d'approcher les performances obtenues par des bibliothèques numériques comme LAPACK. À un plus haut niveau, ces routines nous permettent de valider la réutilisation de codes spécifiques sur un problème classique du calcul formel: la résolution de systèmes linéaires diophantiens. La bibliothèque LinBox est disponible à www.linalg.org.
  • Keywords:

    exact linear algebra, finite field, algorithm analysis, algorithm design, numerical libraries, interfaces, generic programming, matrix factorization, diophantine linear system..
    Keywords (in french):

    algèbre linéaire exacte, corps finis, analyse algorithmique, développement algorithmique, bibliothèques numériques, interfaces, programmation générique, factorisations de matrices, systèmes linéaires diophantiens..
  • Availability: Electronic copy only.
  • Size: 206p
  • Format: pdf
  • Get it

Types pour des langages de programmation orientée d'objet et fonctionnelle.

  • By: Silvia Likavec
  • Number: PhD2004-10
  • Date: Décembre 2004
  • Abstract:

    This thesis consists of three parts. The first part presents three extensions of Bono et al.'s ``Core calculus of classes and mixins". The first extension is a proposal for a programming language equipped with higher-order mixins, which enables the construction of sophisticated class hierarchies. In the second extension mixins are seen as incomplete classes, and accordingly, their instances are seen as incomplete objects that could be completed in an object-based fashion via method addition and object composition. In the third extension, width subtyping on complete object types is added to the calculus of mixins and incomplete objects. The second part studies the untyped $\overline{\lambda}\mu\widetilde{\mu}$ (\lmm) calculus. The confluence of \lmmT and \lmmQ, two well-behaved subcalculi of \lmm, closed under call-by-name and call-by-value reduction respectively, is proved. Moreover, the interpretation of \lmmT in the category of negated domains, and the interpretation of \lmmQ in the Kleisli category is given. To the best of our knowledge, this is the first interpretation of untyped \lmm calculus. In the third part, two inverse limit lambda models are constructed, which completely characterize the sets of terms with similar computational behaviors: the sets of normalizing, head normalizing, weak head normalizing lambda terms, those corresponding to the persistent versions of these notions, and the sets of closable, closable normalizing, and closable head normalizing \lambda terms.
  • Abstract (in french):

    La thèse est divisée en trois parties. La première partie présente deux extensions du ``Core calculus of Classes and Mixins'' de Bono et al. La première extension est une proposition de langage de programmation équipé de mixins d'ordre supérieur, qui permet la construction de hiérarchies de classes sophistiquées. Dand la second extension, les mixins sont vus comme des classes incomplètes et en conséquence, leurs instances sont des objets incomplets qui peuvent ensuite être complétés au niveau des objets par ajout de méthode et composition d'objets. La seconde partie étudie le $\overline{\lambda}\mu\widetilde{\mu}$ calcul (\lmm) non typé. On prouve la confluence de \lmmT et \lmmQ, deux sous-calculs de \lmm dotés de bonnes propriétés et clos par réduction en appel par nom et en appel par valeur, respectivement. De plus, on donne l'interprétation de \lmmT dans la catégorie des ``domaines niés'' et l'interprétation de \lmmQ dans la catégorie de Kleisli. A notre connaissance, cela constitue la première interpétation non typée du \lmm calcul. Dans la troisième partie, nous construisons deux lambda modèles avec limite inverse qui caractérisent complètement des ensembles de termes dotés de comportements calculatoires semblables: les termes normalisants, ceux qui admettent une forme normale de tête, ceux qui admettent une forme normale de tête faible, les ensembles de termes correspondant aux versions persistentes de ces notions, ainsi que les ensembles de terms qui admettent la fermeture, la fermeture normalisant et la fermeture normalisant de tête.
  • Keywords:

    Type theory, object-orientation, compositionality, mixins, classes, objects, continuation semantics, classical logic, categories, domains, models, intersection types, reducibility method.
  • Availability: Electronic copy only.
  • Size: 288p
  • Format: ps
  • Get it