Cette thèse décrit comment l'ajout de trois ingrédients à Système Fω permet d'écrire des programmes de façon modulaire dans un système explicite à la Church, tout en gardant un style proche des modules de ML. Le premier chapitre s'intéresse aux types existentiels ouverts, qui confèrent la possibilité d'utiliser des types existentiels sans restriction de portée : cela offre une plus grande flexibilité dans l'organisation des programmes. Le deuxième chapitre est consacré à l'étude des kinds singletons, qui modélisent les définitions de types : dans ce cadre, on donne une caractérisation simple de l'équivalence de types, fondée sur une relation de réduction confluente et fortement normalisante. Le dernier chapitre intègre les deux notions précédentes dans un langage noyau muni d'une relation de sous-typage : cela apporte à Fω un gain de modularité important, de niveau comparable à celui des modules de ML. Une traduction des modules vers ce langage est esquissée, permettant une comparaison précise des deux langages.

<p>NestStep is a collection of parallel extensions to existing programming languages. These extensions supports a shared memory model and nested parallelism. NestStep is based the Bulk-Synchronous Programming model. Most of the communication of data in NestStep takes place in a</p><p>combine/commit phase, which is essentially a reduction followed by a broadcast.</p><p>The primary aim of the project that this thesis is based on was to develop a runtime system for NestStep-C, the extensions for the C programming language. The secondary aim was to find which tree structure among a selected few is the best for communicating data in the combine/commit phase.</p><p>This thesis includes information about NestStep, how to interface with the NestStep runtime system, some example applications and benchmarks for determining the best tree structure. A binomial tree structure and trees similar to it was empirically found to yield the best performance.</p>

Spreadsheet languages are the most commonly used end-user programming paradigm, yet spreadsheets commonly contain errors. Research shows that a significant number of spreadsheets (20%-40%) created by end users contain errors. In an attempt to reduce this error rate, this work presents an assertion propagation system for an end-user spreadsheet programming language, along with proofs of correctness, and complexity analysis. In addition to the traditional benefits of assertions (dynamic error checking and the documentation of programmer assumptions) this system deductively propagates the implications of assertions. This propagation adds two benefits, the cross-checking of program logic, and additional immediate visual feedback about the range of behavior of the program code for the end-user. / Graduation date: 2002

Researchers in the Forms/3 group have previously developed the WYSIWYT methodology, exploring a way of systematically testing spreadsheet languages. The previous work presented the WYSIWYT methodology for individual spreadsheet cells, and later partially extended it to large grids in which some cells share the same formula. The Forms/3 spreadsheet language supports not only operations of individual cells but also some advanced programming features such as homogeneous grids, recursive programs, and user-defined abstract data types. Therefore, it is important for the testing methodology to support even these more powerful features of the language, not just the "easy parts". In this document, we present extensions to the WYSIWYT methodology for these advanced features. We optimized the visual aspects of testing spreadsheet grids and collected experimental information about scalability. We also developed two possible ways the WYSIWYT methodology could be extended to accommodate recursion in terms of their testing theoretic aspects, implementation strategies, algorithms and time complexities. Since the ultimate goal is to help the people using these languages, we also conducted an empirical study and used its results to inform our choice as to which of these two approaches to adopt. Finally, we developed an approach of testing user-defined abstract data types; here we present design, implementation issues, algorithms and time complexities. / Graduation date: 2002

E-commerce has begun to evolve beyond simple web pages to more sophisticated ways of conducting e-business transactions, such as through electronic advertising, negotiation, and delivery. However, to participate in these advances requires the skills of professional programmers, and end-user owners of small businesses often cannot justify this expense. In this thesis, we present FAR, an end-user language to offer and deliver e-services. The novel aspects of FAR are its support of small e-services and its multiparadigm approach to combining ideas from spreadsheets and rule-based programming with drag-and-drop web page layout devices. / Graduation date: 2002

How can rigorous forms of testing be supported in a way that is both compatible with the visual aspect of visual programming languages, and usable by the audiences using those languages - even when the audience has no background in software engineering? Visual programs are likely to contain at least some errors, and supporting a visual form of testing would give users a way to spot those errors early in the program's life. In previous work, we have developed a visual testing methodology known as WYSIWYT, for use in visual spreadsheet languages, and in this work, we show formally that this methodology can be generalized to screen transition diagrams. The algorithms and accompanying proof of the coverage equivalence that they ensure provide the mechanisms needed for the screen transition paradigm to incorporate WYSIWYT testing for both professional and end-user programming audiences. / Graduation date: 2004 / Best scan available for figures. Original is blurry.

How might capabilities for algorithm animation be seamlessly integrated into a programming language that is both visual and declarative? Until now, visual programming language researchers have not attempted to answer that question, making the fruits of algorithm animation available only to users of textual programming languages. Users of visual programming languages (VPLs) have been deprived of the unique semantic insights algorithm animation offers, insights that would foster the understanding and debugging of visual programs. We have answered the question by seamlessly integrating algorithm animation capabilities into Forms/3, a general-purpose, declarative VPL. Our results show that such a VPL can support algorithm animation without leaving the declarative, visual model, without adding new concepts to the language or how to program in it, and without deviating from the uniform representation established for the language. In addition, our research shows that the characteristics of declarative VPLs result in some interesting algorithm animation features not found in other systems. / Graduation date: 1995

Graduation date: 2006 / Functional programming is concerned with referential transparency, that is, given a certain function and its parameter, that the result will always be the same. However, it seems that this is violated in applications involving uncertainty, such as rolling a dice. This thesis defines the background of probabilistic programming and domain-specific languages, and builds on these ideas to construct a domain-specific embedded language (DSEL) for probabilistic programming in a purely functional language. This DSEL is then applied in a real-world setting to develop an application in use by the Center for Gene Research at Oregon State University. The process and results of this development are discussed.

Cette thèse décrit une nouvelle approche pour la méta-programmation sûre. Un méta-programme est un programme qui manipule des programmes ou assimilés. Les compilateurs et systèmes de preuves sont de bons exemples de méta-programmes qui bénéficieraient de cette approche. Dans ce but, ce travail se concentre sur la représentation des noms et des lieurs dans les structures de données. Les erreurs de programmation étant courantes avec les techniques usuelles, nous proposons une interface abstraite pour les noms et les lieurs qui élimine ces erreurs. Cette interface est implémentée sous forme d'une bibliothèque en Agda. Elle permet de définir et manipuler des représentations de termes dans le style nominal. Grâce à l'abstraction, d'autres styles sont aussi disponibles : le style de De Bruijn, les combinaisons de ces styles, et d'autres encore. Nous indiçons les noms et les termes par des mondes. Les mondes sont en même temps précis et abstraits. Via les relations logiques et la paramétricité, nous pouvons démontrer dans quel sens notre bibliothèque est sûre, et obtenir des "théorèmes gratuits" à propos des fonctions monde-polymorphiques. Ainsi une fonction monde-polymorphique de transformation de termes doit commuter avec n'importe quel renommage des variables libres. La preuve est entièrement conduite en Agda. Notre technique se montre utile sur plusieurs exemples, dont la normalisation par évaluation qui est connue pour être un défi. Nous montrons que notre approche indicée par des mondes permet d'exprimer un large panel de type de données grâce a des langages de définition embarqués.

La programmation par aspects est un paradigme de programmation qui permet de mieux séparer les préoccupations d'une application. Un aspect est défini pour chaque préoccupation qui ne peut pas être isolée dans un module. Les aspects sont ensuite ajoutés au programme de base par un processus automatique appelé tissage. Cependant, l'expressivité des langages d'aspect généraux permet de modifier totalement la sémantique du programme de base (par ex., un aspect peut remplacer certains appels de méthode par du code arbitraire). Ce comportement peut entraîner la perte des avantages (lisibilité, maintenabilité, réutilisabilité, etc.) d'une meilleure modularisation des préoccupations. Il devient impossible de raisonner sur le programme de base sans regarder le programme tissé. Cette thèse apporte une réponse aux problèmes ci-dessus en définissant des catégories d'aspects dont l'impact sur la sémantique du programme de base reste sous contrôle. Pour chaque catégorie d'aspects, nous déterminons l'ensemble des propriétés du programme de base qui est préservé par tissage. L'appartenance d'un aspect à une catégorie est garantie par construction grâce à des langages d'aspect dédiés pour chaque catégorie. L'utilisation de ces langages assure que le tissage préservera l'ensemble des propriétés associé à la catégorie concernée. Les propriétés préservées sont représentées comme des sous ensembles de LTL et de CTL*. Nous prouvons formellement que quelque soit le programme de base, le tissage de n'importe quel aspect d'une catégorie préserve les propriétés de la catégorie correspondante. Ces langages et catégories sont définis dans un cadre formel indépendant de tout langage de base ou d'aspect. L'expressivité de ce cadre est montrée en décrivant des primitives complexes de langages d'aspect comme AspectJ et CaesarJ et en effectuant une preuve de correction de transformation d'aspect.