PEPM

Two trends are emerging in the World Wide Web (WWW). The first is the proliferation of Web Services -- self-contained, Web-accessible software applications and associated distributed systems architectures. The second is the emergence of the "Semantic ...

This paper presents an offline partial evaluator for the λ-calculus with the delimited continuation constructs shift and reset. Based on Danvy and Filinski's type system for shift and reset, we first present a type system that specifies well-annotated ...

A powerful application of specialization is to remove interpretative overhead: a language can be implemented with an interpreter, whose performance is then improved by specializing it for a given program source. This approach is only moderately ...

The use of partial evaluation for specializing programs written in imperative languages such as C and Java is hampered by the difficulty of controlling the specialization process. We have developed a simple, declarative language for controlling the ...

Component-Based Software Development (CBSD)is an attractive way to deliver generic executable pieces of program, ready to be reused in many different contexts. Component reuse is based on a black-box model that frees component consumers from diving into ...

Automated program transformation holds promise for a variety of software life cycle endeavors, particularly where the size of legacy systems makes code analysis, re-engineering, and evolution very difficult and expensive. But constructing transformation ...

Working with High Assurance (HA) and Distributed, Real-time Embedded (DRE) applications, we have found numerous opportunities for software specialization. The problem has been that partial evaluation (PE) alone is insufficient to carry out all the ...

Programmers frequently write program generators using the simple model of programs as text. The essence of this approach is its lack of structure. For this reason, it gets no respect from academic researchers. But the flip side of lacking structure is ...

Standard operating systems provide only a single fixed scheduler, which does not meet all possible application scheduling needs. More flexibility can be achieved using a hierarchy of schedulers, allowing multiple schedulers to coexist in a single ...

Program generation is among the most promising techniques in the effort to increase the automation of programming tasks. In this paper, we discuss the potential impact and research value of program generation, we give examples of our research in the ...

We propose a new algorithm for fusion transformation that allows both stacks and accumulating parameters. The new algorithm can fuse programs that cannot be handled by existing fusion techniques, eg, XML transformations. The algorithm is formulated in a ...

We implement strength reduction and loop-invariant code motion by specializing instrumented interpreters; we define a novel program transformation that uses bisimulation to identify and remove code duplication in residual programs; and we discover that ...

Tracing computations is a widely used methodology for program debugging. Lazy languages, in particular, pose new demands on tracing techniques since following the actual trace of a computation is generally useless. Typically, they rely on the ...

We present a new method, based on a form of dependent typing, to verify the correct usage of resources in a program. Our approach allows complex resources to be specified, whose properties are captured by annotated types and conditions on invariance and ...

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CafeOBJ, Maude, and equational subsets of ELAN and CASL. ...

We address the problem of proving total correctness of transformation rules for definite logic programs. We consider a general transformation rule, called clause replacement, which consists in transforming a program P into a new program Q by replacing a ...

In this paper we introduce a novel scheme for portable CPU accounting and control in Java, which is based on program transformation techniques at the bytecode level and can be used with every standard Java Virtual Machine. In our approach applications, ...

This paper presents a novel editor supporting interactive refinement in the development of structured documents. The user performs a sequence of editing operations on the document view, and the editor automatically derives an efficient and reliable ...

We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access policy specification. We then proceed to specialise the ...

Although electronic computers are the only "computer species" we are accustomed to, the mathematical notion of a programmable computer has nothing to do with wires and logic gates. In fact, Alan Turing's notional computer, which marked in 1936 the birth ...

blast is an automatic verification tool for checking temporal safety properties of C~programs. blast is based on lazy predicate abstraction driven by interpolation-based predicate discovery. The blast specification language specifies program properties ...

Proof-carrying code (PCC) was introduced by George Necula and Peter Lee in 1996. The principle is simple: we can eliminate the need to trust code by forcing the producer to give us a formal, machine-checkable proof that the code won't exhibit some "bad ...