Abstract When writing transformation systems, a significant amount of engineering effort goes into setting up the infrastructure needed to direct individual transformations to specific targets in the data being transformed. Strategic programming languages provide general-purpose infrastructure for this task, which the author of a transformation system can use for any algebraic data structure. The Kansas University Rewrite Engine (KURE) is a typed strategic programming language, implemented as a Haskell-embedded domain-specific language. KURE is designed to support typed transformations over typed data, and the main challenge is how to make such transformations compatible with generic traversal strategies that should operate over any type. Strategic programming in a typed setting has much in common with datatype-generic programming . Compared to other approaches to datatype-generic programming, the distinguishing feature of KURE's solution is that the user can configure the behaviour of traversals based on the location of each datum in the tree, beyond their behaviour being determined by the type of each datum. This article describes KURE's approach to assigning types to generic traversals, and the implementation of that approach. We also compare KURE, its design choices, and their consequences, with other approaches to strategic and datatype-generic programming.

Adequate encodings are a powerful programming tool, which eliminate whole classes of program bugs: they ensure that a program cannot generate ill-formed data, because such data is not part of the representation; and they also ensure that a program is well-defined, meaning that it cannot have different behaviors on different representations of the same piece of data. Unfortunately, it has proven difficult to define adequate encodings of programming languages themselves. Such encodings would be very useful in language processing tools such as interpreters, compilers, model-checking tools, etc., as these systems are often difficult to get correct. The key problem in representing programming languages is in encoding binding constructs; previous approaches have serious limitations in either the operations they allow or the correcness guarantees they make. In this paper, we introduce a new library for Haskell that allows the user to define and use higher-order encodings, a powerful technique for representing bindings. Our library allows straightforward recursion on bindings using pattern-matching, which is not possible in previous approaches. We then demonstrate our library on a medium-sized example, lambda-lifting, showing how our library can be used to make strong correctness guarantees at compile time.

The Rosetta system specification language will require a variety of analysis capabilities to assist system designers. The language's generality prohibits the development of a single analysis tool. It is proposed, instead, to leverage the existing analysis tools and create an analysis environment unified around the Rosetta language. A semi-automated tool, the Rosetta Nexus, will generated tool-specific analysis models and a correspondence with the original Rosetta specifications.

Modular Monadic Semantics (MMS) is a well-known mechanism for structuring modular denotational semantic definitions for programming languages. The principal attraction of MMS is that families of language constructs can be independently specified and later combined in a mix-and-match fashion to create a complete language semantics. This has proved useful for constructing formal, yet executable, semantics when prototyping languages. In this work we demonstrate that MMS has an additional software engineering benefit. Rather than composing semantics for various language constructs, we can use MMS to compose various differing semantics for the same language constructs. We describe algebra combinators, the principal vehicle for achieving this reuse, along with a series of applications of the technique for common language processing tasks.

Modular monadic semantics (MMS) is a well-known technique for structuring modular denotational semantic definitions. Families of language constructs are independently defined using syntactic functors and semantic algebras that can be combined in a mix-and-match fashion to create complete language definitions. We introduce InterpreterLib, a Haskell library that implements and extends MMS techniques for writing composable analyses. In addition to modular analyses composition, InterpreterLib provides algebra combinators, explicit algebra semantics, preprocessors for boiler plate generation and generic programming techniques adapted to language analysis. The key benefits of these features are reliability, increased code reuse via modularity and the ability to rapidly retarget component analyses.