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.

No description available.

In this thesis we describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on ‘schemes’, which are formulae in higher-order logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of a theory can be used, not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory-formation systems. We exploit associative-commutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.

Software is becoming a pervasive presence in our lives, powering computing systems in the home, in businesses, and in safety-critical settings. In response, languages are being defined with support for new domains and complex computational abstractions. The need for formal techniques to help better understand the languages we use, correctly design new language abstractions, and reason about the behavior and correctness of programs is now more urgent then ever. In this dissertation we focus on research in programming language semantics and program analysis, aimed at building and reasoning about programming languages and applications. In language semantics, we first show how to use formal techniques during language design, presenting definitional techniques for object-oriented languages with concurrency features, including the Beta language and a paradigmatic language called KOOL. Since reuse is important, we then present a module system for K, a formalism for language definition that takes advantage of the strengths of rewriting logic and term rewriting techniques. Although currently specific to K, parts of this module system are also aimed at other formalisms, with the goal of providing a reuse mechanism for different forms of modular semantics in the future. Finally, since performance is also important, we show techniques for improving the executable and analysis performance of rewriting logic semantics definitions, specifically focused on decisions around the representation of program values and configurations used in semantics definitions. The work on performance, with a discussion of analysis performance, provides a good bridge to the second major topic, program analysis. We present a new technique aimed at annotation-driven static analysis called policy frameworks. A policy framework consists of analysis domains, an analysis generic front-end, an analysis-generic abstract language semantics, and an abstract analysis semantics that defines the semantics of the domain and the annotation language. After illustrating the technique using SILF, a simple imperative language, we then describe a policy framework for C. To provide a real example of using this framework, we have defined a units of measurement policy for C. This policy allows both type and code annotations to be added to standard C programs, which are then used to generate modular analysis tasks checked using the CPF semantics in Maude.

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.

No description available.

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.

Nous introduisons la stratégie de réécriture de termes k-bornée (bo(k), pour k entier) pour les systèmes linéaires. Cette stratégie est associée à une classe de systèmes dits k-bornés LBO(k). Nous démontrons que les systèmes de la classe LBO (union des LBO(k) pour tous les k), inversent-préservent la reconnaissabilité. Nous montrons que les différents problèmes de terminaison et d'inverse-terminaison pour la stratégie bo(k) sont décidables et utilisons ce résultat pour démontrer la décidabilité de ces problèmes pour des sous-classes de LBO: les classes de systèmes linéaires fortement k-bornés: LFBO(k). La classe LFBO (union des LFBO(k)) inclut strictement de nombreuses classes de systèmes connues: les systèmes inverses basiques à gauche, linéaires growing, et linéaires inverses Finite-Path-Overlapping. Le problème de l'appartenance à LFBO(k) est décidable alors qu'il ne l'est pas pour LBO(0). Pour les mots, nous prouvons que la stratégie bo(k) préserve l'algébricité. Nous étendons la notion de réécriture k-bornée aux systèmes de réécriture de termes linéaires à gauche. Comme dans le cas linéaire, nous associons à cette stratégie la classe des systèmes linéaires à gauche k-bornés BO(k) qui étend la classe LBO(k). Nous démontrons que les systèmes de cette classe inverse-préservent la reconnaissabilité.Comme dans le cas linéaire, nous définissons ensuite la classe des systèmes fortement kbornés FBO(k), qui étend la classe LFBO(k). Nous montrons que le problème de l'appartenance à FBO(k) est décidable. La classe FBO contient strictement la classe des systèmes growing linéaires à gauche. / We introduce k-bounded term rewriting for linear systems (bo(k), for k integer). This strategy is associated with the class of k-bounded systems LBO(k). We show that the systems in the class LBO (union of the LBO(k) for all k), inverse-preserve recognizability. We show that the problems of termination and inverse-termination for the bo(k) strategy are decidable and use this result to show the decidability of these two problems for subclasses of LBO: the classes of linear systems strongly k-bounded: LFBO(k). The class LFBO (union of the LFBO(k)) includes strictly many known classes: the inverse left-basic systems, the linear growing systems, the linear inverse Finite-Path-Overlapping systems. Membership to LFBO(k) is decidable but this is not hte case for LBO(0). For words, we show that the bo(k) strategy preserves algebricity. We extend k-bounded rewriting to left-linear systems. As in the linear case, we associate a class of systems to the strategy: the class of left-linear kbounded systems BO(k) which extends LBO(k). We show that the systems in BO(k) inversepreserve recognizability. As in the linear case, we define the class of strongly k-bounded systems FBO(k), which extends LFBO(k). Membership to FBO(k) is proved decidable. The FBO class contains stricly the class of left-linear growing systems.

We present a term rewriting procedure based on congruence closure that can be used with arbitrary equational theories. This procedure is motivated by the pragmatic need to prove equations in equational theories where confluence can not be achieved. The procedure uses context free grammars to represent equivalence classes of terms. The procedure rewrites grammars rather than terms and uses congruence closure to maintain certain congruence properties of the grammar. Grammars provide concise representations of large term sets. Infinite term sets can be represented with finite grammars and exponentially large term sets can be represented with linear sized grammars.

Biological data is accumulated at a fast pace. However, raw data are generally difficult to understand and not useful unless we unlock the information hidden in the data. Knowledge/information can be extracted as the patterns or features buried within the data. Thus data mining, aims at uncovering underlying rules, relationships, and patterns in data, has emerged as one of the most exciting fields in computational science. In this dissertation, we develop efficient approaches to the structure pattern analysis of RNA and protein three dimensional structures. The major techniques used in this work include term rewriting and clustering algorithms. Firstly, a new approach is designed to study the interaction of RNA secondary structures motifs using the concept of term rewriting. Secondly, an improved K-means clustering algorithm is proposed to estimate the number of clusters in data. A new distance descriptor is introduced for the appropriate representation of three dimensional structure segments of RNA and protein three dimensional structures. The experimental results show the improvements in the determination of the number of clusters in data, evaluation of RNA structure similarity, RNA structure database search, and better understanding of the protein sequence-structure correspondence.