Thesis (Ph. D.)--University of Wisconsin--Madison, 1984. / Typescript. Vita. eContent provider-neutral record in process. Description based on print version record. Includes bibliographical references (leaves 416-438).

Digitized by Kansas Correctional Industries

Thesis (M.A.)--University of Delaware, 2007. / Principal faculty advisors: J. Ritchie Garrison and Ronald W. Fuchs, II, Winterthur Program in Early American Culture. Includes bibliographical references.

Thesis (M.S.)--Worcester Polytechnic Institute. / Keywords: Maude; term rewriting; access control. Includes bibliographical references (leaves 36-37).

Term rewriting -- an expressive language based on equational logic -- can be used to author and analyze policies that are part of an access control system. Maude is a simple, yet powerful, reflective programming language based on term rewriting that models systems along with the subjects, objects and actions within them. We specify the behavior of the system as a theory defined by conditional rewrite rules, and define the access control policy as an equational theory in a separate module. The tools that Maude provides, such as the Maude Model Checker and the Sufficient Completeness Checker, are used to reason about the behavior and verify properties of access control systems in an automated manner.

Today’s market competitiveness and globalisation are putting pressure on organisations to join their efforts, to focus more on cooperation and interaction and to add value to their businesses. That is, most information systems supporting these cross-organisations are characterised as service-oriented business applications, where all the emphasis is put on inter-service interactions rather than intra-service computations. Unfortunately for the development of such inter-organisational service-oriented business systems, current service technology proposes only ad-hoc, manual and static standard web-service languages such as WSDL, BPEL and WS-CDL [3, 7]. The main objective of the work reported in this thesis is thus to leverage the development of service-oriented business applications towards more reliability and dynamic adaptability, placing emphasis on the use of business rules to govern activities, while composing services. The best available software-engineering techniques for adaptability, mainly aspect-oriented mechanisms, are also to be integrated with advanced formal techniques. More specifically, the proposed approach consists of the following incremental steps. First, it models any business activity behaviour governing any service-oriented business process as Event-Condition-Action (ECA) rules. Then such informal rules are made more interaction-centric, using adapted architectural connectors. Third, still at the conceptual-level, with the aim of adapting such ECA-driven connectors, this approach borrows aspect-oriented ideas and mechanisms, and proposes to intercept events, select the properties required for interacting entities, explicitly and separately execute such ECA-driven behavioural interactions and finally dynamically weave the results into the entities involved. To ensure compliance and to preserve the implementation of this architectural conceptualisation, the work adopts the Maude language as an executable operational formalisation. For that purpose, Maude is first endowed with the notions of components and interfaces. Further, the concept of ECA-driven behavioural interactions are specified and implemented as aspects. Finally, capitalising on Maude reflection, the thesis demonstrates how to weave such interaction executions into associated services.

Synthesis planning is a critical process in chemical design. A number of computer programs have been developed to assist the chemists with this procedure. Most of the programs utilize combinations of computational approaches. These have been successfully applied to a number of the synthesis predictions. However, they require numerous rules to screen for potential targets, as well as to keep the system from reaching the combinatorial explosion. This results in the advanced algorithms becoming more complex and parameter-sensitive. This can be problematic, particularly in the cases in which a large number of the compounds are to be handled, because it can not only result in a lengthy computational time, but also cause some of the highly potential targets to be missed. We developed a simpler approach for the reaction prediction using a term-rewriting grammar. The term-rewriting strategy is used to directly assign reactions to the compounds. This greatly reduces the number of rules that are usually required for these steps, and, hence, facilitates the prediction performance, while maintaining the prediction accuracy. In this dissertation, the designs of the developed algorithms and their results are first being presented, followed by a discussion of the approach’s application in the chemical design in the final chapter.

[ES] La evaluación parcial de programas es una técnica general y potente de optimización de programas que preserva su semántica y tiene muchas aplicaciones relevantes. La optimización se consigue al especializar programas con respecto a una parte de sus datos de entrada, lo que produce un nuevo programa llamado residual o programa especializado tal que, al ejecutarlo con los datos de entrada restantes, producirá el mismo resultado que produce el programa original con todos sus datos de entrada. Los esquemas de evaluación parcial existentes no son aplicables a lenguajes expresivos basados en reglas como Maude, CafeOBJ, OBJ, ASF+SDF y ELAN, los cuales soportan: 1) sofisticados tipos estructurados con subtipos y sobrecarga de operadores; y 2) teorías ecuacionales modulo varias combinaciones de axiomas tales como asociatividad, conmutatividad e identidad. Esta tesis desarrolla las bases teóricas necesarias e ilustra los conceptos principales para su aplicación a programas expresivos escritos en el lenguaje Maude. El esquema de evaluación parcial presentado en esta tesis está basado en un algoritmo automático de desplegado que computa variantes de términos. Para asegurar la terminación del proceso de especialización se han diseñado algoritmos de alto rendimiento para la generalización ecuacional menos general con tipos ordenados y subsunción homeomórfica ecuacional con tipos ordenados. Se muestra que la técnica de evaluación parcial desarrollada es correcta y completa para teorías de reescritura convergentes que pueden contener varias combinaciones de axiomas de asociatividad, conmutatividad y/o identidad para diferentes operadores binarios. Finalmente se presenta Victoria, el primer evaluador parcial para teorías ecuacionales de tipos ordenados para el lenguaje Maude, y se demuestra la efectividad y el incremento en eficiencia ganado a través de experimentos realizados con ejemplos reales. / [CAT] L'avaluació parcial de programes és una tècnica general i potent d'optimització de programes que preserva la seua semàntica i té moltes aplicacions rellevants. L'optimització s'aconseguix a l'especialitzar programes respecte a una part de les seues dades d'entrada, la qual cosa produïx un nou programa cridat residual o programa especialitzat tal que, a l'executar-ho amb les dades d'entrada restants, produirà el mateix resultat que produïx el programa original amb totes les seues dades d'entrada. Els esquemes d'avaluació parcial existents no són aplicables a llenguatges expressius basats en regles com Maude, CafeOBJ, OBJ, ASF+SDF i ELAN, els quals suporten: 1) sofisticats tipus estructurats amb subtipus i sobrecàrrega d'operadors; i 2) teories equacionals mòdul diverses combinacions d'axiomes com asociativitat, conmutativitat i identitat. Esta tesi desenrotlla les bases teòriques necessàries i il·lustra els conceptes principals per a la seua aplicació a programes expressius escrits en el llenguatge Maude. L'esquema d'avaluació parcial presentat en esta tesi està basat en un algoritme automàtic de desplegat que computa variants de termes. Per a assegurar la terminació del procés d'especialització s'han dissenyat algoritmes d'alt rendiment per a la generalització ecuacional menys general amb subtipus ordenats i subsunción ecuacional homeomórfica amb subtipus ordenats. Es mostra que la tècnica d'avaluació parcial desenrotllada és correcta i completa per a teories de reescriptura convergents que poden contindre diverses combinacions d'axiomes d'asociativitat, conmutativitat i identitat per a diferents operadors binaris. Finalment es presenta Victoria, el primer avaluador parcial per a teories equacionals de tipus ordenats per al llenguatge Maude i es demostra l'efectivitat i l'increment en eficiència guanyat a través d'experiments realitzats amb exemples reals. / [EN] Partial evaluation is a powerful and general program optimization technique that preserves program semantics and has many successful applications. Optimization is achieved by specializing programs w.r.t. a part of their input data so that, when the residual or specialized program is executed on the remaining input data, it produces the same outcome than the original program with all of its input data. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with sorts, subsorts, and overloading; and 2) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity. This thesis develops the new foundations needed and illustrates the key concepts of equational order sorted partial evaluation by showing how they apply to the specialization of expressive programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on high-performance order-sorted equational least general generalization and ordersorted equational homeomorphic embedding algorithms for ensuring termination.We show that our partial evaluation technique is sound and complete for order-sorted equational theories that may contain various combinations of associativity, commutativity, and/or identity axioms for different binary operators. Finally, we present Victoria, the first partial evaluator for Maude's order-sorted equational theories, and demonstrate the effectiveness of our partial evaluation scheme on several examples where it shows significant speed-up. / Finally, I extend my thanks to SENESCYT for the support provided for my studies. Also, I thank the Universidad de Guayaquil that is my place of work. / Cuenca Ortega, ÁE. (2019). Partial Evaluation of Rewriting Logic Theories [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/130206 / TESIS

Ce mémoire de maîtrise porte sur les limites du dévoilement de soi et des autres dans les écrits autofictionnels. Il examine les conséquences du dévoilement et des processus de censure liés au genre de l’autofiction. La première partie de ce mémoire, La fille de nulle part, est un recueil de poèmes s'articulant autour d'un deuil amoureux. Divisés en cinq parties égales, les poèmes de cette collection explorent les thèmes de l’abandon, de l’estime personnelle et de la vengeance. Adressé à un TU (représentant l'ancien amoureux), ce recueil est porté par la voix d'un JE désabusé et profondément triste. Au fil des poèmes, les différentes étapes du deuil amoureux sont parcourues, sans toutefois conduire à l’acceptation et la reconstruction. Les poèmes sont portés par Paméla Personne, alter ego de la poète Paméla Couture. La deuxième partie de ce mémoire porte sur l'analyse du récit de Maude Veilleux, Prague. Il sera plus précisément question de confronter l’hypothèse suivante : Maude Veilleux n’est pas allée aussi loin que le sous-entendait le pacte de lecture de son récit Prague, quant au dévoilement de soi. Le chapitre premier porte sur les théories littéraires associées à l'autofiction, afin de déterminer si Prague correspond au genre. Les travaux de Vincent Colonna et de David Bélanger serviront de base de recherche pour cette section. Le chapitre deuxième étudie l’utilité et la portée des mensonges et divers évitements dans la fiction, dans le but de cerner l’intention des mensonges et contournements de Prague. Les recherches effectuées par John R. Searle serviront d’appui pour cette partie. Le chapitre troisième teste l'hypothèse du mémoire à l’aide d’entretiens faits avec l'écrivaine Maude Veilleux, à propos de son récit Prague. / This Master's thesis focuses on the limits of self-disclosure and others in autofictional writings. It examines the consequences of disclosure and censorship processes related to the autofictional genre. The first part of this dissertation, La fille de nulle part, is a collection of poems that revolves around a mourning love. Divided into five equal parts, the poems in this collection explore the themes of abandonment, self-esteem, and vengeance. Addressed to a YOU (representing the lost lover), this collection is carried by the voice of a disillusioned and deeply sad I. Throughout the poems, the different stages of the mourning are covered, without leading to acceptance and reconstruction. The poems are carried by Paméla Personne, alter ego of the poet Paméla Couture. The second part of this thesis focuses on the analysis of the story of Maude Veilleux, Prague. It will be more precisely a matter of confronting the following hypothesis: Maude Veilleux did not go as far as the author-reader contract suggested in her story of Prague, as to the disclosure of herself. Chapter One focuses on the literary theories associated to autofiction, to determine whether Prague corresponds to this particular genre. The works of Vincent Colonna and David Bélanger will serve as a research base for this section. The second chapter studies the usefulness and reach of the lies and various avoidances in fiction, in order to determine the intent of the lies and workarounds in Prague. The research done by John R. Searle will support this part. The third chapter tests the hypothesis of the Master through interviews with the writer Maude Veilleux, about her story Prague.

Maude es un lenguaje de programación declarativo basado en la lógica de reescritura que incorpora muchas características que lo hacen muy potente. Sin embargo, a la hora de probar ciertas propiedades computacionales esto conlleva dificultades. La tarea de probar la terminación de sistemas de reesctritura es de hecho bastante dura, pero aplicada a lenguajes de programación reales se concierte en más complicada debido a estas características inherentes. Esto provoca que métodos para probar la terminación de este tipo de programas requieran técnicas específicas y un análisis cuidadoso. Varios trabajos han intentado probar terminación de (un subconjunto de) programas Maude. Sin embargo, todos ellos siguen una aproximación transformacional, donde el programa original es trasformado hasta alcanzar un sistema de reescritura capaz de ser manejado con las técnicas y herramientas de terminación existentes. En la práctica, el hecho de transformar los sistemas originales suele complicar la demostración de la terminación ya que esto introduce nuevos símbolos y reglas en el sistema. En esta tesis, llevamos a cabo el problema de probar terminación de (un subconjunto de) programas Maude mediante métodos directos. Por un lado, nos centramos en la estrategia de Maude. Maude es un lenguaje impaciente donde los argumentos de una función son evaluados siempre antes de la aplicación de la función que los usa. Esta estrategia (conocida como llamada por valor) puede provocar la no terminación si los programas no están escritos cuidadosamente. Por esta razón, Maude (en concreto) incorpora mecanismos para controlar la ejecución de programas como las anotaciones sintácticas que están asociadas a los argumentos de los símbolos. En reescritura, esta estrategia sería conocida como reescritura sensible al contexto innermost (RSCI). Por otro lado, Maude también incorpora la posibilidad de declarar atributos. / Alarcón Jiménez, B. (2011). Towards a Framework for Proving Termination of Maude Programs [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/11003 / Palancia