No description available.

Programmers design, write, and understand programs with a high-level structure in mind. Existing programming languages are not very good at capturing this structure because they must include low-level implementation details. To address this problem we introduce Twig, a programming language that allows for domain-specific logic to be encoded alongside low-level functionality. Twig's language is based on a simple, formal calculus that is amenable to both human and machine reasoning. Users may introduce rules that rewrite expressions, allowing for user-defined optimizations. Twig can also incorporate procedures written in a variety of low-level languages. Our implementation supports C and Python, but our abstract model can accommodate other languages as well. We present Twig's design and formal semantics and discuss our implementation. We demonstrate Twig's use in two different domains, multi-language programming and GPU programming, and compare Twig against a well-known typemapping system, SWIG.

String diagrams provide a convenient graphical framework which may be used for equational reasoning about morphisms of monoidal categories. However, unlike term rewriting, which is the standard way of reasoning about the morphisms of monoidal categories, rewriting string diagrams results in shorter equational proofs, because the string diagrammatic representation allows us to formally establish equalities modulo any rewrite steps which follow from the monoidal structure. Manipulating string diagrams by hand is a time-consuming and error-prone process, especially for large string diagrams. This can be ameliorated by using software proof assistants, such as Quantomatic. However, reasoning about concrete string diagrams may be limiting and in some scenarios it is necessary to reason about entire (infinite) families of string diagrams. When doing so, we face the same problems as for manipulating concrete string diagrams, but in addition, we risk making further mistakes if we are not precise enough about the way we represent (infinite) families of string diagrams. The primary goal of this thesis is to design a mathematical framework for equational reasoning about infinite families of string diagrams which is amenable to computer automation. We will be working with context-free families of string diagrams and we will represent them using context-free graph grammars. We will model equations between infinite families of diagrams using rewrite rules between context-free grammars. Our framework represents equational reasoning about concrete string diagrams and context-free families of string diagrams using double-pushout rewriting on graphs and context-free graph grammars respectively. We will prove that our representation is sound by showing that it respects the concrete semantics of string diagrammatic reasoning and we will show that our framework is appropriate for software implementation by proving important decidability properties.

L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés / The objective of this thesis is to explore formal descriptions for the structure and functioning of biological systems, as well as formal tools for reasoning about their behavior. This work takes place in the overall prospective to study safe computational models where computations are expressed via rewriting, and where we can rely on formal verification to express and validate suitable properties. In this thesis we develop a higher-order calculus rewriting for describing molecules, reaction patterns, and biochemical network generation. The calculus is based on the chemical metaphor by describing the computations in terms of chemical solutions in which molecules representing data freely interact according to reaction rules. This way we obtained an Abstract Biochemical Calculus as an extension of the higher-order chemical model by considering structured molecules. The calculus is provided with a natural specification of concurrency and of controlling mechanisms by expressing rewrite strategies as molecules. The description of molecular complexes or chemical reactants belong to specific classes of graphs. We define the structure of port graphs and we show how the principles of the biochemical calculus instantiated for port graphs are expressive enough for modeling autonomous systems and biochemical networks. In addition, strategic rewriting techniques open the way to reason about the computations and to verify properties of the modeled systems

軟體即服務（Software as a Service, SaaS）是雲端運算環境下一種新興的服務模式，它的特色是將特定的應用軟體以共享軟硬體資源的方式供眾多的租戶（tenants）使用。因此，如何提供共用且有客制化功能的應用軟體就是SaaS模式的重要成功關鍵。本研究聚焦於資料庫層提供多租戶共用表格但有客制化功能的機制。讓開發人員延續一租戶一資料表的架構為基礎設計資料庫，透過SQL語句轉換機制，將SQL語句轉換為操作共享表格的語句執行，以大幅減化開發人員的工作。本研究包含兩個部份，一是資料綱要對應表(Schema Mapping Table)，協助開發人員將單租戶資料庫架構轉換為塊狀表格(chunk table)的共用資料綱要方式；另一個是SQL語句自動轉換工具，透過剖面技術織入JDBC程式集中，在應用系統執行期間，將SQL語句，從一租戶一資料表寫法轉換為共享表格的方式執行。故只需將資料表改為共用架構即可使用，達到提升多租戶系統開發速度並提高資源使用率的目的。 / Software as a service (SaaS) is an emerging service model of cloud computing, which is characterized by providing software that charges on a usage basis over shared hardware and software resources for a large number of tenants to use. Therefore, how to provide shared tables and customization of the applications is an important key to success in the SaaS model. This study focuses on how to enable multi-tenancy on the database layer Developers can extend a private table structure-based application to a shared database one through the proposed SQL rewriting mechanism. This approach can greatly simplify the developer's work. Our approach consists of two parts, first is Schema Mapping Table that helps developers to convert single-tenant database architecture into the chunk table schema; another is SQL statement conversion tools that works by enhancing the JDBC library as an aspect in the AspectJ language. During the execution of the application, a SQL statement is rewritten from the private table based format into chunk table based statement. In this way, we are able to enhance an application with multitenant shared tables that improve resource utilization.

No description available.

Thesis (Ph.D.)--Hong Kong University of Science and Technology, 2008. / Includes bibliographical references (p. 120-125). Also available in electronic version.

Thesis (M.Sc.) - Carleton University, 2005. / Includes bibliographical references (p. 61-63). Also available in electronic format on the Internet.

Thesis (MSc)--University of Stellenbosch, 2008. / Bibliography. Also available via the Internet.

Submitted by Suelen Reis (suziy.ellen@gmail.com) on 2013-05-17T11:35:37Z No. of bitstreams: 1 Tese Carlos da Silva.pdf: 4459786 bytes, checksum: 0d5ee6a2e39d0afc3bff06cbd7f106eb (MD5) / Approved for entry into archive by Alda Lima da Silva(sivalda@ufba.br) on 2013-05-23T18:37:25Z (GMT) No. of bitstreams: 1 Tese Carlos da Silva.pdf: 4459786 bytes, checksum: 0d5ee6a2e39d0afc3bff06cbd7f106eb (MD5) / Made available in DSpace on 2013-05-23T18:37:25Z (GMT). No. of bitstreams: 1 Tese Carlos da Silva.pdf: 4459786 bytes, checksum: 0d5ee6a2e39d0afc3bff06cbd7f106eb (MD5) Previous issue date: 2007 / Esta tese investiga a reescritura do universo literário de Virginia Woolf para a literatura e para o cinema, por meio da observação das reescrituras do romance Mrs. Dalloway (1925): o filme Sra. Dalloway (1997), de Marleen Gorris; o livro As Horas (1998), de Michael Cunningham; e o filme As Horas (2002), de Stephen Daldry. Partimos da hipótese de que as narrativas reescritoras são mais tradicionais, têm novo arranjo linear e não seguem uma tendência vanguardista, devido, principalmente, ao estilo dos tradutores. Para comprovarmos tal hipótese, analisamos algumas estratégias de tradução, empregadas na criação de imagens de Woolf para os novos públicos, levantando, em cada narrativa, questões gerais sobre o enredo e a construção do tempo e do espaço. As estratégias observadas, no filme Sra. Dalloway, foram as seguintes: linearidade (organização narrativa), flashback, voice-over e montagem. No filme As Horas as estratégias foram as seguintes: delineação do enredo (criação de três histórias paralelas), continuidade de elementos imagéticos (montagem), silêncio e expressões dos atores/atrizes e múltiplas perspectivas. A análise levou-nos a concluir que essas narrativas têm formatos próprios (como arranjo linear particular) e não seguem a tendência vanguardista do texto de Woolf, devido às questões inerentes ao meio cinematográfico (ampliação de público, criação de narrativas lineares, influência da narrativa clássica hollywoodiana, etc), mas, principalmente, devido ao estilo e concepção de criação dos próprios tradutores. A análise fundamenta-se na idéia de reescritura de Lefevere (1992), como um tipo de tradução, na concepção de tradução dos Estudos Descritivos de Toury (1995) e da teoria dos polissistemas de Even-Zohar (1990) e em alguns estudos que tratam da relação literatura e cinema, tais como Bordwell (1985), Vanoye & Goliot-Lété (1994), Aumont et al (1995) e Cruz (1997). / Salvador