2,199 papers · page 84 of 110
It is widely agreed that recursive types are inherent in the static typing of the essential mechanisms of object-oriented programming: encapsulation, message passing, subtyping, and inheritance. We demonstrate here that modeling object encapsulation in terms of existential types …
In many kinds of emnputatiomd contexts, modifications of the input data are to be processed at once so as to have immediate effect on the output. Because small changes in the input to a computation often cause only small changes in the outpu~ the challenge is to compute the new o…
We consider the following problem in proving observational congruences in functional languages: given a call-by-name language based on the simply-typed λ-calculus with algebraic operations axiomatized by algebraic equations E, is the set of observational congruences between terms…
No abstract available.
To separately compile a program module in traditional statically-typed languages, one has to manually write down an import interface which explicitly specifies all the external symbols referenced in the module. Whenever the definitions of these external symbols are changed, the m…
No abstract available.
We describe and prove algorithms to convert programs which use the Parallel Computing Forum Parallel Sections construct into Static Single Assignment (SSA) form. This proces allows compilers to apply classical scalar optimization algorithms to explicitly parallel programs. To do …
Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conv…
According to folklore, Algol is an “orthogonal” extension of a simple imperative programming language with a call-by-name functional language. The former contains assignments, branching constructs, and compound statements; the latter is based on the typed λ-calculus. In an attemp…
We have designed and implemented an interprocedural program analyzer generator, called system Z. Our goal is to automate the generation and management of semantics-based interprocedural program analysis for a wide range of target languages.
This paper describes algorithms for inserting monitoring code to profile and trace programs. These algorithms greatly reduce the cost of measuring programs with respect to the commonly used technique of placing code in each basic block. Program profiling counts the number of time…
LR parsing techniques have long been studied as efficient and powerful methods for processing context free languages. A linear time algorithm for recognizing languages representable by LR(k) grammars has long been known. Recognizing substrings of a context-free language is at lea…
We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such th…
ion Robert Cartwright Matthias Felleisen Department of Computer Science Rice University Houston, TX 77251-1892 Rice Technical Report CS 91-167 A preliminary version of this technical report appeared in the Proceedings of the 19th Annual ACM Symposium on Principles of Programming …
Traditional optimization techniques for sequential programs are not directly applicable to parallel programs where concurrent activities may interfere with each other through shared variables. New compiler techniques must be developed to accommodate features found in parallel lan…
We describe a method for using abstraction to reduce the complexity of temporal logic model checking. The basis of this method is a way of constructing an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can …
This paper contains a full treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. Surprisingly enough the results obtained contradict the common-place feeling that (the core of) ML is a subset of second order λ-calculus: we can…
We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can be specified, at various le…