title: Macro-by-Example: Deriving Syntactic Transformations from their Specifications

authors:
Eugene E. Kohlbecker
Mitchell Wand

abstract: This paper presents two new developments. First, it describes a “macro-by-example” specification language for syntactic abstractions in Lisp and related languages. This specification language allows a more declarative specification of macros than conventional macro facilities do by giving a better treatment of iteration and mapping constructs. Second, it gives a formal semantics for the language and a derivation of a compiler from the semantics. This derivation is a practical application of semantics-directed compiler development methodology.


venue: popl

title: On Strictness and its Analysis

authors:
Tsung-Min Kuo
Prateek Mishra

abstract: We study the strictness problem for the untyped lambda-calculus and for an ML-like typed calculus. We establish that strictness is a necessary and sufficient condition for the “eager” evaluation of function arguments. For the untyped calculus, we show that the strictness problem is elementary and describe a complete algorithm for strictness analysis of convergent terms. We show that typed terms possess a much richer set of strictness properties. A type-theoretic characterization of strictness is developed and it is shown that the strictness properties of a term can be represented as a collection of types related to the standard term type. A set of type inference rules that support reasoning about strictness related types is given. The inference rules are shown to be invariant under type change by substitution. This provides a sound basis for reasoning about strictness properties of terms by considering only their principal type. For our final result, we describe a practical system that carries out type checking and strictness analysis simultaneously in a unified framework. Our main result is thus the discovery that the problem of strictness analysis is a particular case of type inference.


title: A Realistic Compiler Generator Based on High-Level Semantics

authors:
Peter Lee
Uwe F. Pleban

abstract: We have developed a new style of semantic definition called high-level semantics. In constrast to traditional denotational semantics, high-level semantics is suitable for both defining the functional meaning of programming languages, as well as describing realistic compiler implementations. Moreover, high-level specifications are considerably more descriptive and intelligible than traditional specifications.


title: Skinny and Fleshy Failures of Relative Completeness

authors:
Daniel Leivant
Tim Fernando

abstract: The notion of relative completeness of logics of programs was delineated almost ten years ago, in particular by Wand, Cook and Clarke. More recently, it has been felt that Cook's notion hinges on a fragile balance between the semantics of a programming language and first-order expressiveness in structures. This fragility underlies the negative results about relative completeness.


title: Specification and Verification of Concurrent Programs By Forall-Automata

authors:
Zohar Manna
Amir Pnueli

abstract: ∀-automata are non-deterministic finite-state automata over infinite sequences. They differ from conventional automata in that a sequence is accepted if all runs of the automaton over the sequence are accepting. These automata are suggested as a formalism for the specification and verification of temporal properties of concurrent programs. It is shown that they are as expressive as extended-temporal-logic (ETL), and in some cases provide a more compact representation of properties than temporal logic. A structured diagram notation is suggested for the graphical representation of these automata. A single sound and complete proof rule is presented for proving that all computations of a program have the property specified by a ∀-automaton.


title: Empty Types in Polymorphic Lambda Calculus

authors:
Albert R. Meyer
John C. Mitchell
Eugenio Moggi
Richard Statman

abstract: The model theory of simply typed and polymorphic (second-order) lambda calculus changes when types are allowed to be empty. For example, the “polymorphic Boolean” type really has exactly two elements in a polymorphic model only if the “absurd” type ∀t.t is empty. The standard β-ε axioms and equational inference rules which are complete when all types are nonempty are not complete for models with empty types. Without a little care about variable elimination, the standard rules are not even sound for empty types. We extend the standard system to obtain a complete proof system for models with empty types. The completeness proof is complicated by the fact that equational “term models” are not so easily obtained: in contrast to the nonempty case, not every theory with empty types is the theory of a single model.


title: A Logic for Partially Specified Data Structures

authors:
M. Drew Moshier
William C. Rounds


title: Computation of Aliases and Support Sets

authors:
Anne Neirynck
Prakash Panangaden
Alan J. Demers

abstract: We provide a scheme for determining which global variables are involved when an expression is evaluated in a language with higher order constructs and imperative features. The heart of our scheme is a mechanism for computing the support of an expression, i.e. the set of global variables involved in its evaluation. This computation requires knowledge of all the aliases of an expression. The inference schemes are presented as abstract semantic interpretations. We prove the soundness of our estimates by establishing a correspondence between the abstract semantics and the standard semantics of the programming language.


title: Strictness Analysis and Denotational Abstract Interpretation

abstract: A theory of abstract interpretation [CoCo79] is developed for a typed λ-calculus. The typed λ-calculus is the “static” part of a two-level denotational metalanguage for which abstract interpretation was developed in [Nie86]. The present development relaxes a condition imposed in [Nie86] and this suffices to make the framework applicable to strictness analysis for the λ-calculus. This shows the possibility of a general theory (and hence a system) for the analysis of functional programs. Furthermore, it gives more insight into the relative precision of the various analyses. In particular, it is shown that a collecting (static [CoCo79]) semantics exists, thus answering a problem left open in [BHA86].


title: Semantics for Concurrency without Powerdomains

abstract: Article Free Access Share on Semantics for concurrency without powerdomains Author: F. J. Oles Mathematical Sciences Department, IBM Thomas J. Watson Research Center, Yorktown Heights, New York Mathematical Sciences Department, IBM Thomas J. Watson Research Center, Yorktown Heights, New YorkView Profile Authors Info & Claims POPL '87: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesOctober 1987 Pages 211–222https://doi.org/10.1145/41625.41644Published:01 October 1987Publication History 4citation169DownloadsMetricsTotal Citations4Total Downloads169Last 12 Months9Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: The Concurrent Logic Programming Language CP: Definition and Operational Semantics

abstract: In this paper we present some of the control constructs of the language CP, which is based on a concurrent interpretation of Horn logic programming. We present a formal structural operational semantics and relate the meaning of programs in this language to the underlying (pure) Horn clause axioms.


title: Concurrent Transition System Semantics of Process Networks

abstract: Using concurrent transition systems [Sta86], we establish connections between three models of concurrent process networks, Kahn functions, input/output automata, and labeled processes. For each model, we define three kinds of algebraic operations on processes: the product operation, abstraction operations, and connection operations. We obtain homomorphic mappings, from input/output automata to labeled processes, and from a subalgebra (called “input/output processes”) of labeled processes to Kahn functions. The proof that the latter mapping preserves connection operations amounts to a new proof of the “Kahn Principle.” Our approach yields: (1) extremely simple definitions of the process operations; (2) a simple and natural proof of the Kahn Principle that does not require the use of “strategies” or “scheduling arguments”; (3) a semantic characterization of a large class of labeled processes for which the Kahn Principle is valid, (4) a convenient operational semantics for nondeterminate process networks.


title: Computable Values Can Be Classical

authors:
Val Tannen
Albert R. Meyer

abstract: In programming languages of universal power, the computational integers must be distinguished from the classical integers because of the “divergent” integer. Even the equational theory corresponding to evaluation of integer expressions is distinct from the theory of classical integers, and classical reasoning about computational integers yields inconsistencies. We show that there exist “programming languages”, actually extensions of the polymorphic lambda calculus, that have tremendous computing power and yet whose computational integers, or any other algebraically specified abstract data type, coincide with their classical counterpart. In particular, the equational theory of the programming language is a conservative extension of the theory of the underlying base types as given by algebraic data type specifications.


title: Views: A Way for Pattern Matching to Cohabit with Data Abstraction

abstract: Pattern matching and dta abstraction are important concepts in designing programs, but they do not it well together. Pattern matching depend on making public a free data type mpresentaiion, while data abstraction depends on hiding the repreentaiion. This paper proposes the vdws mechanism at a means of reconc'dlng this conflict. A view allows any type to be viewed at a free data type, thus combining the clarity of pattern matching with the eiclency of data abstraction.


title: Completeness and Incompleteness of Trace-Based Network Proof Systems

authors:
Jennifer Widom
David Gries
Fred B. Schneider

abstract: Abstract. Most trace-based proof systems for networks of processes are known to be incomplete. Extensions to achieve completeness are generally complicated and cumbersome. In this paper, a simple trace logic is defined and two examples are presented to show its inherent incompleteness. Surprisingly, both examples consist of only one process, indicating that network composition is not a cause of incompleteness. Axioms necessary and sufficient for the relative completeness of a trace logic are then presented.


title: Detecting Equality of Variables in Programs

authors:
Bowen Alpern
Mark N. Wegman
F. Kenneth Zadeck

abstract: Article Free Access Share on Detecting equality of variables in programs Authors: B. Alpern IBM Thomas J. Watson Research Center, Yorktown Heights, NY IBM Thomas J. Watson Research Center, Yorktown Heights, NYView Profile , M. N. Wegman IBM Thomas J. Watson Research Center, Yorktown Heights, NY IBM Thomas J. Watson Research Center, Yorktown Heights, NYView Profile , F. K. Zadeck Department of Computer Science, Brown University, Providence, RI Department of Computer Science, Brown University, Providence, RIView Profile Authors Info & Claims POPL '88: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1988 Pages 1–11https://doi.org/10.1145/73560.73561Published:13 January 1988Publication History 264citation2,559DownloadsMetricsTotal Citations264Total Downloads2,559Last 12 Months137Last 6 weeks21 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Bisimulation Can't Be Traced

authors:
Bard Bloom
Sorin Istrail
Albert R. Meyer

abstract: Bisimulation is the primitive notion of equivalence between concurrent processes in Milner's Calculus of Communicating Systems (CCS); there is a nontrivial game-like protocol for distinguishing nonbisimular processes. In contrast, process distinguishability in Hoare's theory of Communicating Sequential Processes (CSP) is determined solely on the basis of traces of visible actions. We examine what additional operations are needed to explain bisimulation similarly—specifically in the case of finitely branching processes without silent moves. We formulate a general notion of Structured Operational Semantics for processes with Guarded recursion (GSOS), and demonstrate that bisimulation does not agree with trace congruence with respect to any set of GSOS-definable contexts. In justifying the generality and significance of GSOS's, we work out some of the basic proof theoretic facts which justify the SOS discipline.


title: A Compositional Approach to Superimposition

authors:
Luc Bougé
Nissim Francez

abstract: A general definition of the notion of superimposition is presented. We show that previous constructions under the same name can be seen as special cases of our definition. We consider several properties of superimposition definable in our terms, notably the nonfreezing property. We also consider a syntactic representation of our construct in CSP


title: Structural Subtyping and the Notion of Power Type

abstract: types We have used the term abstract type for types of the form P = Some(A:Type) B, because this models the concept of having an unknown type A which supports a set of operations of signature B. It should be pointed out that, unlike abstract types in second-order lambda calculus [Mitchell Plotkin 85] this notion of type abstraction does not prevent impersonation. That is, given a particular implementation p = pair(A:Type = C) b:B of P, the representation type C is visible, hence one can build an object of type A without using the operations in b. This problems can be partially solved by scoping techniques; e.g., a function which must operate on arbitrary implementations of P cannot make assumptions about any particular C. A complete solution to the impersonation problem requires introducing additional concepts [MacQueen 86]. On the positive side, the fact that even abstract types are matched by structure means that redefining an abstract type does not create a "new" one. This is co...


title: Incremental Data Flow Analysis via Dominator and Attribute Updates

authors:
Martin D. Carroll
Barbara G. Ryder

abstract: We present an algorithm for updating data flow information derived from a program, in response to program edits. Our algorithm, applicable to intraprocedural or interprocedural data flow problems, is more general than previous methods because it can update any monotone data flow problem defined on a reducible flow graph and can handle arbitrary program edits.Rather than design yet another special-purpose data flow update algorithm, we show how to reduce the class of data flow problems to another class of problems which already has a fast update algorithm. More specifically, we reduce a monotone data flow problem formulated for solution using Graham-Wegman elimination [12] to the problem of constructing and decorating an attributed tree structurally isomorphic to the dominator tree of the program flow graph.To update this dominator tree in response to program changes, we first show how to express domination in terms of two local properties of nodes and edges in the flow graph — niceness and deepness. Domination is then updated in response to an edge addition or deletion by repeatedly performing two local operations on the dominator tree, each operation restoring the local properties violated by the edge change. Second, we extend Reps' attributed tree update techniques [19,21,20] and his complexity analysis, to update attribute values in response to changes in this structure.


title: Efficient Dataflow Analysis of Logic Programs

abstract: We investigate a framework for efficient flow analyses of logic programs. A major problem in this context is that unification can give rise to aliasing and dependencies between variables whose effects are difficult to predict, and which make sound flow analysis algorithms computationally expensive. We give a simple characterization of the class of flow analysis problems for which aliasing effects can be ignored without loss of soundness, and describe an efficient analysis procedure for this class of problems. The utility of our approach is illustrated by discussing its application to several analysis and optimization problems for logic programs. Our results are useful in the design of efficient flow analysis systems for logic programming languages.


title: The Theory and Practice of First-Class Prompts

abstract: An analysis of the λugr;-C-calculus and its problematic relationship to operational equivalence leads to a new control facility: the prompt-application. With the introduction of prompt-applications, the control calculus becomes a traditional calculus all of whose equations imply operational equivalence. In addition, prompt-applications enhance the expressiveness and efficiency of the language. We illustrate the latter claim with examples from such distinct areas as systems programming and tree processing.


title: Inductive Methods for Reasoning about Abstract Data Types

authors:
Stephen J. Garland
John V. Guttag

abstract: Rewriting techniques have been used to reason about a variety of topics related to programming languages, e.g., abstract data types, Petri Nets, FP programs, and data bases. They have also been used in the implementation and definition of a variety of programming languages.


title: Integrating Non-Interfering Versions of Programs

authors:
Susan Horwitz
Jan F. Prins
Thomas W. Reps

abstract: The need to integrate several versions of a program into a common one arises frequently, but it is a tedious and time consuming task to integrate programs by hand. The main contribution of this paper is an algorithm, called integrate, that takes as input three programs A, B, and Base, where A and B are two variants of Base. Whenever the changes made to Base to create A and B do not “interfere” (in a sense defined in the paper), Integrate produces a program M that integrates A and B.


title: On the Adequacy of Program Dependence Graphs for Representing Programs

abstract: Program dependence graphs were introduced by Kuck as an intermediate program representation well suited for performing optimizations, vectorization, and parallelization. There are also additional applications for them as an internal program representation in program development environments.


title: A Collecting Interpretation of Expressions (Without Powerdomains)

authors:
Paul Hudak
Jonathan Young

abstract: A collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a denotational framework is akin to traditional data flow analysis, and when used in the context of abstract interpretation allows one to infer properties that approximate the run-time behavior of expression evaluation. In this paper collecting interpretations of expressions are developed for three abstract functional languages: (1) a first-order language with call-by-value semantics, (2) a first-order language with call-by-name semantics, and (3) a higher-order language with call-by-name semantics (i.e., the full untyped lambda calculus with constants). It is argued that the method is simple (in particular, no powerdomains are needed), natural (it captures the intuitive operational behavior of a cache), yet more expressive than existing methods (it is the first exact collecting interpretation for either lazy or higher-order programs).


title: Supernode Partitioning

authors:
François Irigoin
Rémi Triolet

abstract: Supercompilers must reschedule computations defined by nested DO-loops in order to make an efficient use of supercomputer features (vector units, multiple elementary processors, cache memory, etc…). Many rescheduling techniques like loop interchange, loop strip-mining or rectangular partitioning have been described to speedup program execution. We present here a class of partitionings that encompasses previous techniques and provides enough flexibility to adapt code to multiprocessors with two levels of parallelism and two levels of memory.


title: Stores and Partial Continuations as First-Class Objects in a Language and its Environment

authors:
Gregory F. Johnson
Dominic Duggan


title: Inheritance in Smalltalk-80: A Denotational Definition

abstract: A denotational semantic definition of SMALLTALK-80 is given. Its most notable characteristic is a surprisingly simple treatment of inheritance. An executable version of the semantics, written in STANDARD ML, is also described.


title: A Proper Extension of ML with an Effective Type-Assignment

authors:
A. J. Kfoury
Jerzy Tiuryn
Pawel Urzyczyn

abstract: We extend the functional language ML by allowing the recursive calls to a function F on the right-hand side of its definition to be at different types, all generic instances of the (derived) type of F on the left-hand side of its definition. The original definition of ML does not allow this feature. This extension does not produce new types beyond the usual universal polymorphic types of ML and satisfies the properties already enjoyed by ML: the principal-type property and the effective type-assignment property.


title: Compiler Optimizations for Asynchronous Systolic Array Programs

abstract: A programmable systolic array of high-performance cells is an attractive computation engine if it attains the same utilization of dedicated arrays of simple cells. However, typical implementation techniques used in high-performance processors, such as pipelining and parallel functional units, further complicate the already difficult task of systolic algorithm design. This paper shows that high-performance systolic arrays can be used effectively by presenting the machine to the user as an array of conventional processors communicating asynchronously. This abstraction allows the user to focus on the higher level problem of partitioning a computation across cells in the array. Efficient fine-grain parallelism can be achieved by code motion of communication operations made possible by the asynchronous communication model. This asynchronous communication model is recommended even for programming algorithms on systolic arrays without dynamic flow control between cells.The ideas presented in the paper have been validated in the compiler for the Warp machine [4]. The compiler has been in use in various application areas including robot navigation, low-level vision, signal processing and scientific programming. Near-optimal code has been generated for many published systolic algorithms.


title: Polymorphic Effect Systems

authors:
John M. Lucassen
David K. Gifford

abstract: We present a new approach to programming languages for parallel computers that uses an effect system to discover expression scheduling constraints. This effect system is part of a 'kinded' type system with three base kinds: types, which describe the value that an expression may return; effects, which describe the side-effects that an expression may have; and regions, which describe the area of the store in which side-effects may occur. Types, effects and regions are collectively called descriptions.


title: Towards Fully Abstract Semantics for Local Variables

authors:
Albert R. Meyer
Kurt Sieber

abstract: The Store Model of Halpern-Meyer-Trakhtenbrot is shown—after suitable repair—to be a fully abstract model for a limited fragment of ALGOL in which procedures do not take procedure parameters. A simple counter-example involving a parameter of program type shows that the model is not fully abstract in general. Previous proof systems for reasoning about procedures are typically sound for the HMT store model, so it follows that theorems about the counter-example are independent of such proof systems. Based on a generalization of standard cpo based models to structures called locally complete partial orders (lcpo's), improved models and stronger proof rules are developed to handle such examples.


title: The Essence of ML

authors:
John C. Mitchell
Robert Harper

abstract: Standard ML is a useful programming language with polymorphic expressions and a flexible module facility. One notable feature of the expression language is an algorithm which allows type information to be omitted. We study the implicitly-typed expression language by giving a “syntactically isomorphic” explicitly-typed, polymorphic function calculus. Unlike the Girard-Reynolds polymorphic calculus, for example, the types of our ML calculus may be built-up by induction on type levels (universes). For this reason, the pure ML calculus has straightforward set-theoretic, recursion-theoretic and domain-theoretic semantics, and operational properties such as the termination of all recursion-free programs may be proved relatively simply. The signatures, structures, and functors of the module language are easily incorporated into the typed ML calculus, providing a unified framework for studying the major features of the language (including the novel “sharing constraints” on functor parameters). We show that, in a precise sense, the language becomes inconsistent if restrictions imposed by type levels are relaxed. More specifically, we prove that the important programming features of ML cannot be added to any impredicative language, such as the Girard-Reynolds calculus, without implicitly assuming a type of all types.


title: Correct Flow Analysis in Continuation Semantics

authors:
Margaret Montenyohl
Mitchell Wand

abstract: Three semantics-preserving transformations (static replacement, factoring, and combinator selection) are used to convert a continuation semantics into a formal description of a semantic analyzer and code generator. The result of this derivation is a compilation algorithm which performs type checking before code generation so that type-checking instructions are not generated in the target code. Both the flow analysis and the resulting optimizations are proved correct with respect to the original definition of the source language. The proof consists of showing that all restructuring transformations preserve the semantics of the source language. This transformational approach can be extended to derive correctness proofs of other flow analysis and code optimization techniques.


title: Automatic Binding Time Analysis for a Typed Lambda-Calculus

authors:
Hanne Riis Nielson
Flemming Nielson

abstract: For a typed λ-calculus we develop an algorithm that, given some partial information about what must happen at run-time, will work out what actually can be computed at compile-time and what must be deferred to run-time.


title: Optimal Code Generation for Expression Trees: An Application of BURS Theory

authors:
Eduardo Pelegrí-Llopart
Susan L. Graham

abstract: A Rewrite System is a collection of rewrite rules of the form α β where α and β are tree patterns. A rewrite system can be extended by associating a cost with each rewrite rule, and by defining the cost of a rewrite sequence as the sum of the costs of all the rewrite rules in the sequence. The REACHABILITY problem for a rewrite system R is, given an input tree T and a fixed goal tree G, to determine if there exists a rewrite sequence in R, rewriting T into G and, if so, to obtain one such sequence. The C-REACHABILITY problem is similar except that the obtained sequence must have minimal cost among all those sequences writing T into G.


title: Global Value Numbers and Redundant Computations

authors:
Barry K. Rosen
Mark N. Wegman
F. Kenneth Zadeck

abstract: Article Free Access Share on Global value numbers and redundant computations Authors: B. K. Rosen IBM Thomas J. Watson Research Center, Yorktown Heights, NY IBM Thomas J. Watson Research Center, Yorktown Heights, NYView Profile , M. N. Wegman IBM Thomas J. Watson Research Center, Yorktown Heights, NY IBM Thomas J. Watson Research Center, Yorktown Heights, NYView Profile , F. K. Zadeck Department of Computer Science, Brown University, Providence, RI Department of Computer Science, Brown University, Providence, RIView Profile Authors Info & Claims POPL '88: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1988 Pages 12–27https://doi.org/10.1145/73560.73562Published:13 January 1988Publication History 278citation1,997DownloadsMetricsTotal Citations278Total Downloads1,997Last 12 Months240Last 6 weeks26 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Lifetime Analysis of Dynamically Allocated Objects

authors:
Cristina Ruggieri
Thomas P. Murtagh

abstract: The choice of binding time disciplines has major consequences for both the run-time efficiency of programs and the convenience of the language expressing algorithms. Late storage binding time, dynamic allocation, provides the flexibility necessary to implement the complex data structures common in today's object oriented style of programming. In this paper we show that compile-time lifetime analysis can be applied to programs written in languages with static type systems and dynamically allocated objects, to provide earlier storage binding time for objects, while maintaining all the advantages of dynamic allocation.


title: Type Inference with Subtypes

abstract: We give an algorithm for type inference in a language with functions, records, and variant records. A similar language was studied by Cardelli who gave a type checking algorithm. This language is interesting because it captures aspects of object-oriented programming using subtype polymorphism. We give a type system for deriving types of expressions in the language and prove the type inference algorithm is sound, i.e., it returns a type derivable from the proof system. We also prove that the type the algorithm finds is a “principal” type, i.e., one which characterizes all others. The approach taken here is due to Milner for universal polymorphism. The result is a synthesis of subtype polymorphism and universal polymorphism.


title: A Temporal Fixpoint Calculus

abstract: Two distinct extensions of temporal logic has been recently advocated in the literature. The first extension is the addition of fixpoint operators that enable the logic to make assertions about arbitrary regular events. The second extension is the addition of past temporal connectives that enables the logic to refer directly to the history of the computation. Both extensions are motivated by the desire to adapt temporal logic to modular, i.e., compositional, verification (as opposed to global verification). We introduce and study here the logic μTL, which is the extension of temporal logic by fixpoint operators and past temporal connectives. We extend the automata-theoretic paradigm to μTL. That is, we show how, given an μTL formula @@@@, we can produce a finite-state Büchi automaton A@@@@, whose size is at most exponentially bigger than the size of @@@@, such that A@@@@ accepts precisely the computations that satisfy @@@@. The result has immediate applications, e.g., an optimal decision procedure and a model-checking algorithm for μTL.


title: Strictness Analysis Aids Time Analysis

abstract: Analyzing time complexity of functional programs in a lazy language is problematic, because the time required to evaluate a function depends on how much of the result is “needed” in the computation. Recent results in strictness analysis provide a formalisation of this notion of “need”, and thus can be adapted to analyse time complexity.The future of programming may be in this paradigm: to create software, first write a specification that is clear, and then refine it to an implementation that is efficient. In particular, this paradigm is a prime motivation behind the study of functional programming. Much has been written about the process of transforming one functional program into another. However, a key part of the process has been largely ignored, for very little has been written about assessing the efficiency of the resulting programs.Traditionally, the major indicators of efficiency are time and space complexity. This paper focuses on the former.Functional programming can be split into two camps, strict and lazy. In a strict functional language, analysis of time complexity is straightforward, because of the following compositional rule:The time to evaluate (ƒ(g x)) equals the time to evaluate (g x) plus the time to evaluate (ƒ y), where y is the value of (g x).However, in a lazy language, this rule only gives an upper bound, possibly a crude one. For example, if ƒ is the head function, then (g x) need only be evaluated far enough to determine the first element of the list, and this may take much less time than evaluating (g x) completely.The key to a better analysis is to describe formally just how much of the result “needs” to be evaluated; we call such a description a context. Recent results in strictness analysis show how such contexts can be modelled using the domain-theoretic notion of a projection [WH87]. This paper describes how these results can be applied to the analysis of time complexity. The method used was inspired by work of Bror Bjerner on the complexity analysis of programs in Martin-Luf's type theory [Bje87]. The main contribution of this paper is to simplify Bjerner's notation, and to show how contexts can replace his “demand notes”.The language used in this paper is a first-order language. This restriction is made because context analysis for higher-order languages is still under development. An approach to higher-order context analysis is outlined in [Hug87b]. Context analysis is based on backwards analysis, rather than the earlier approach of abstract interpretation; both are discussed in [AH87].Some work on complexity analysis [Weg75,LeM85] has concentrated on automated analysis: algorithms that derive a closed form for the time complexity of a program. The goal here is less ambitious. We are simply concerned with describing a method of converting a functional program into a series of equations that describe its time complexity. This modest beginning is a necessary precursor to any automatic analysis. The time equations can be solved by traditional methods, yielding either an exact solution, an upper bound, or an approximate solution. (Incidentally, although [LeM85] claims to analyse a lazy language, the analysis uses exactly the composition rule above, and so is more suited for a strict language.)The analysis given here involves two kinds of equations. First are equations defining projection transformers that specify how much of a value is “needed”. Second are equations that specify the time complexity; these depend on the projection transformers defined by the first equations.In both cases, we will be more concerned with setting up the equations that with finding their solutions. As already noted, traditional methods may be applied to satisfy the time complexity equations. Solving the projection transformer equations is more problematic. In some cases, we can find an appropriate solution by choosing an appropriate finite domain of projections, and then applying the method of [WH87] to find the solution in this domain. In other cases, no finite domain of solutions is appropriate, and we will find a solution by a more ad-hoc method: guessing one and verifying that it satisfies the required conditions. More work is required to determine what sort of solutions to the projection transformer equations will be most useful for time analysis, and how to find these solutions.This paper is organized as follows. Section 1 describes the language to be analysed. Section 2 presents the evaluation model. Section 3 gives a form of time analysis suitable for strict evaluation. Section 4 shows how projections can describe what portion of a value is “needed”, and introduces projection transformers. Section 5 gives the time analysis for lazy evaluation. Section 6 presents a useful extension to the analysis method. Section 7 concludes.


title: Sacrificing Simplicity for Convenience: Where Do You Draw the Line?

authors:
John H. Williams
Edward L. Wimmers

abstract: The designers of (functional) programming languages are faced with two occasionally conflicting goals: programmer convenience and semantic simplicity. For example, it is convenient to treat I/O operations as primitive “functions” with side effects, but doing so destroys referential transparency.FL is a functional language that is designed to trade some of the semantic simplicity of a pure language for some of the convenience of a procedural language, by treating I/O operations as primitives with “side effects”, but by using a structuring technique that localizes the scope of those effects. In this way, surprisingly little of the semantic simplicity is lost, as can be seen by comparing the underlying algebraic laws of FL with those of its pure counterpart. FP.This paper describes that comparison and shows that, in fact, for programs involving I/O, the structures of the algebraic laws of the two languages are identical! It concludes by showing that this technique cannot be extended to allow assignment statements without incurring a massive loss in the expressiveness and simplicity of the underlying algebra.


title: Dynamic Typing in a Statically-Typed Language

authors:
Martín Abadi
Luca Cardelli
Benjamin C. Pierce
Gordon D. Plotkin

abstract: Statically-typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type-consistency checks are performed at runtime. However, even in statically-type languages, there is often the need to deal with data whose type cannot be known at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T. Instances of Dynamic are built with an explicit tagging construct and inspected with a type-safe typecase construct.


title: Continuation-Passing, Closure-Passing Style

authors:
Andrew W. Appel
Trevor Jim

abstract: We implemented a continuation-passing style (CPS) code generator for ML. Our CPS language is represented as an ML datatype in which all functions are named and most kinds of ill-formed expressions are impossible. We separate the code generation into phases that rewrite this representation into ever-simpler forms. Closures are represented explicitly as records, so that closure strategies can be communicated from one phase to another. No stack is used. Our benchmark data shows that the new method is an improvement over our previous, abstract-machine based code generator.


title: Synthesis of Concurrent Systems with Many Similar Sequential Processes

authors:
Paul C. Attie
E. Allen Emerson

abstract: Methods for synthesizing concurrent programs from Temporal Logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson & Clarke [EC82] and Manna & Wolper [MW84]. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. One only has to formulate a precise problem specification; the synthesis method then mechanically constructs a correct solution. A serious drawback of these methods in practice, however, is that they suffer from the state explosion problem. To synthesize a concurrent system consisting of K sequential processes, each having N states in its local transition diagram, requires construction of the global product-machine having at least NK global states in general. This exponential growth in K makes it infeasible to synthesize systems composed of more than 2 or 3 processes. In this paper, we show how to synthesize concurrent systems consisting of many (i.e., a finite but arbitrarily large number K of) similar sequential processes. Our approach avoids construction of the global product-machine for K processes; instead, it constructs a two process product-machine for a single pair of generic sequential processes. The method is uniform in K, providing a simple template that can be instantiated for each process to yield a solution for any fixed K. The method is also illustrated on synchronization problems from the literature.


title: Temporal Logic Programming is Complete and Expressive

abstract: This paper addresses semantic and expressiveness issues for temporal logic programming and in particular for the TEMPLOG language proposed by Abadi and Manna. Two equivalent formulations of TEMPLOG's declarative semantics are given: in terms of a minimal Herbrand model and in terms of a least fixpoint. By relating these semantics to TEMPLOG's operational semantics, we prove the completeness of the resolution proof system underlying TEMPLOG's execution mechanism. To study TEMPLOG's expressiveness, we consider its propositional version. We show how propositional TEMPLOG programs can be translated into a temporal fixpoint calculus and prove that they can express essentially all regular properties of sequences.


title: The Program Dependence Graph and Vectorization

authors:
William Baxter
Henry R. Bauer III

abstract: Previous attempts at vectorizing programs written in a sequential high level language focused on converting control dependences to data dependences using a mechanism known as IF-conversion. After IF-conversion vector optimizations are performed on a data dependence graph. However, IF-conversion is an irrevocable process which can introduce high run-time overhead if the input program is not amenable to vectorization.


title: The Modula-3 Type System

authors:
Luca Cardelli
James E. Donahue
Mick J. Jordan
Bill Kalsow
Greg Nelson

abstract: This paper presents an overview of the programming language Modula-3, and a more detailed description of its type system.


title: Fast Interprocedural Alias Analysis

authors:
Keith D. Cooper
Ken Kennedy

abstract: We present a new algorithm for computing interprocedural aliases due to passing parameters by reference. This algorithm runs in O(N2+NE) time and, when combined with algorithms for alias-free, flow-insensitive data-flow problems, yields algorithms for solution of the general flow-insensitive problems that also run in O(N2+NE) time.


title: An Efficient Method of Computing Static Single Assignment Form

authors:
Ron Cytron
Jeanne Ferrante
Barry K. Rosen
Mark N. Wegman
F. Kenneth Zadeck

abstract: Article An efficient method of computing static single assignment form Share on Authors: R. Cytron IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NYView Profile , J. Ferrante IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NYView Profile , B. K. Rosen IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NYView Profile , M. N. Wegman IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NYView Profile , F. K. Zadeck Computer Science Dept., Brown University, Providence, RI Computer Science Dept., Brown University, Providence, RIView Profile Authors Info & Claims POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1989 Pages 25–35https://doi.org/10.1145/75277.75280Online:03 January 1989Publication History 308citation1,950DownloadsMetricsTotal Citations308Total Downloads1,950Last 12 Months119Last 6 weeks14 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Rewrite, Rewrite, Rewrite, Rewrite, Rewrite

authors:
Nachum Dershowitz
Stéphane Kaplan

abstract: We study properties of rewrite systems that are not necessarily terminating, but allow instead for transfinite derivations that have a limit.In particular, we give conditions for the existence of a limit and for its uniqueness and relate the operational and algebraic semantics of infinitary theories.We also consider sufficient completeness of hierarchical systems.


title: Efficient Temporal Reasoning

authors:
E. Allen Emerson
Tom Sadler
Jai Srinivasan

abstract: There has been much interest in decision procedures for testing satisfiability (or validity) of formulae in various systems of Temporal Logic. This is due to the potential applications of such decision procedures to mechanical reasoning about correctness of concurrent programs. We show that there exist Temporal Logics that are (i) decidable in polynomial time, and (ii) still useful in applications. One surprising corollary of our results is that the fragment of CTL (Computation Tree Logic) actually used by Emerson & Clarke [EC82] to synthesize concurrent programs from temporal specifications is decidable in polynomial time. Another is that the verification of many correctness properties of concurrent programs (such as in Owicki & Lamport [OL82]) can be efficiently automated. This demonstrates that many useful correctness properties can be expressed with a rather restricted syntax. Finally, our results provide insight into the relation between the structural (i.e., syntactic) complexity of temporal logics and the complexity of their decision problems.


title: Fully Abstract Compositional Semantics for Logic Programs

authors:
Haim Gaifman
Ehud Shapiro

abstract: We propose a framework for discussing fully abstract compositional semantics, which exposes the interrelations between the choices of observables, compositions, and meanings. Every choice of observables and compositions determines a unique fully abstract equivalence. A semantics is fully abstract if it induces this equivalence.


title: Copy Elimination in Functional Languages

authors:
K. Gopinath
John L. Hennessy

abstract: Copy elimination is an important optimization for compiling functional languages. Copies arise because these languages lack the concepts of state and variable; hence updating an object involves a copy in a naive implementation. Copies are also possible if proper targeting has not been carried out inside functions and across function calls. Targeting is the proper selection of a storage area for evaluating an expression. By abstracting a collection of functions by a target operator, we compute targets of function bodies that can then be used to define an optimized interpreter to eliminate copies due to updates and copies across function calls. The language we consider is typed lambda calculus with higher-order functions and special constructs for array operations. Our approach can eliminate copies in divide and conquer problems like quicksort and bitonic sort that previous approaches could not handle.


title: CLP* and Constraint Abstraction

abstract: CLP*(D) is a class of constraint logic programming languages which incorporates the notion of abstraction. Predicates in CLP*(D) are (potentially) infinite rational trees which represent abstractions of constraint expressions. This view of predicates as constraint abstractions was motivated by the language Scheme, where closures are viewed as abstractions of functional expressions. A semantics and an efficient implementation of the language are provided, along with several examples of the novel programming techniques provided by this class of languages.


title: A Fully Abstract Trace Model for Dataflow Networks

abstract: A dataflow network consists of nodes that communicate over perfect FIFO channels. For dataflow networks containing only deterministic nodes, a simple and elegant semantic model has been presented by Kahn. However, for nondeterministic networks, the straight-forward generalization of Kahn's model is not compositional. We present a compositional model for nondeterministic networks, which is fully abstract, i.e., it has added the least amount of extra information to Kahn's model which is necessary for attaining compositionality. The model is based on traces.


title: Polymorphic Unification and ML Typing

authors:
Paris C. Kanellakis
John C. Mitchell

abstract: We study the complexity of type inference for a core fragment of ML with lambda abstraction, function application, and the polymorphic let declaration. Our primary technical tool is the unification problem for a class of “polymorphic” type expressions. This form of unification, which we call polymorphic unification, allows us to separate a combinatorial aspect of type inference from the syntax of ML programs. After observing that ML typing is in DEXPTIME, we show that polymorphic unification is PSPACE hard. From this, we prove that recognizing the typable core ML programs is also PSPACE hard. Our lower bound stands in contrast to the common belief that typing ML programs is “efficient,” and to practical experience which suggests that the algorithms commonly used for this task do not slow compilation substantially.


title: Realistic Compilation by Program Transformation

authors:
Richard Kelsey
Paul Hudak

abstract: Using concepts from denotational semantics, we have produced a very simple compiler that can be used to compile standard programming languages and produces object code as efficient as that of production compilers. The compiler is based entirely on source-to-source transformations performed on programs that have been translated into an intermediate language resembling the lambda calculus. The output of the compiler, while still in the intermediate language, can be trivially translated into machine code for the target machine. The compilation by transformation strategy is simple: the goal is to remove any dependencies on the intermediate language semantics that the target machine cannot implement directly. Front-ends have been written for Pascal, BASIC, and Scheme and the compiler produces code for the MC68020 microprocessor.


title: Bisimulation Through Probabilistic Testing

authors:
Kim Guldstrand Larsen
Arne Skou

abstract: We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm with a probability arbitrary close to 1 can distinguish processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2/3-bisimulation — lying strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify an even stronger process relation, called probabilistic bisimulation.


title: Relating Models of Polymorphism

abstract: A new general notion of model for the polymorphic lambda calculus based on the simple idea of a universe, is proposed. Although impossible in nonconstructive set theory, the notion is unproblematic for constructive sets, yields completeness and initiality theorems, and can be used to unify and relate many different notions of model that have been proposed in the literature, including those that extend the basic calculus with additional features such as fixpoints or a type of all types. Moreover, the polymorphic lambda calculus and Martin-Lof type theory are related by a map of logics. A categorical and initial model semantics is given for the basic calculus and for richer calculi that extend the basic one with fixpoints or with a type of all types.


title: Generalized Conjunctive Types

abstract: The definitions of Conjunctive types and their subtype relation, as introduced by Coppo-Dezani, are extended to consider the conjunction as a partial mapping from pairs of types to types, and the subtype relation as a relation between finite sets of types and types. These extensions basically mean that only conjunctions of compatible types are allowed and that the subtype relation is more like, so to speak, the implication in propositional logic. We show that the basic properties of the typing system with conjunctive types are still true. The terms that have a type are exactly the terms that are convertible to a head normal form and it is possible to characterize the terms with normal form by means of the types that are derivable for them in the system. Furthermore, the type assignment defines the interpretation of terms in a very general class of models of the λ-calculus: the models that are based on an information system, as defined by Scott.


title: Unified Algebras and Modules

abstract: This paper concerns the algebraic specification of abstract data types. It introduces and motivates the recently-developed framework of unified algebras, and provides a practical notation for their modular specification. It also compares unified algebras with the well-known framework of order-sorted algebras, which underlies the OBJ specification language.


title: Partial Order Programming

abstract: We introduce a programming paradigm in which statements are constraints over partial orders. A partial order programming problem has the form minimize u subject to u1 ⊒ v1, u2 ⊒ v2, ··· where u is the goal, and u1 ⊒ v1, u2 ⊒ v2, ··· is a collection of constraints called the program. A solution of the problem is a minimal value for u determined by values for u1, v1, etc. satisfying the constraints. The domain of values here is a partial order, a domain D with ordering relation ⊒.


title: Extracting F(omega)'s Programs from Proofs in the Calculus of Constructions

abstract: We define in this paper a notion of realizability for the Calculus of Constructions. The extracted programs are terms of the Calculus that do not contain dependent types. We introduce a distinction between informative and non-informative propositions. This distinction allows the removal of the “logical” part in the development of a program. We show also how to use our notion of realizability in order to interpret various axioms like the axiom of choice or the induction on integers. A practical example of development of program is given in the appendix.


title: On the Synthesis of a Reactive Module

authors:
Amir Pnueli
Roni Rosner

abstract: We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.


title: Incremental Computation via Function Caching

authors:
William W. Pugh
Tim Teitelbaum

abstract: Article Free Access Share on Incremental computation via function caching Authors: W. Pugh Dept. of Computer Science, Cornell University, Ithaca, NY and Dept. of Comp. Sci., Univ. of Maryland, College Park, Md. Dept. of Computer Science, Cornell University, Ithaca, NY and Dept. of Comp. Sci., Univ. of Maryland, College Park, Md.View Profile , T. Teitelbaum Dept. of Computer Science, Cornell University, Ithaca, NY Dept. of Computer Science, Cornell University, Ithaca, NYView Profile Authors Info & Claims POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1989 Pages 315–328https://doi.org/10.1145/75277.75305Published:03 January 1989Publication History 138citation969DownloadsMetricsTotal Citations138Total Downloads969Last 12 Months130Last 6 weeks25 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Typechecking Records and Variants in a Natural Extension of ML

abstract: Strongly typed languages with records may have inclusion rules so that records with more fields can be used instead of records with less fields. But these rules lead to a global treatment of record types as a special case. We solve this problem by giving an ordinary status to records without any ad hoc assertions, replacing inclusion rules by extra information in record types. With this encoding ML naturally extends its polymorphism to records but any other host language will also transmit its power.


title: Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis

authors:
Shmuel Sagiv
Orit Edelstein
Nissim Francez
Michael Rodeh

abstract: Circular attribute grammars appear in many data flow analysis problems. As one way of making the notion useful, an automatic translation of circular attribute grammars to equivalent non-circular attribute grammars is presented. It is shown that for circular attribute grammars that arise in many data flow analysis problems, the translation does not increase the asymptotic complexity of the semantic equations. Therefore, the translation may be used in conjunction with any evaluator generator to automate the development of efficient data flow analysis algorithms. As a result, the integration of such algorithms with other parts of a compiler becomes easier.


title: A Rewriting Semantics for Program Dependence Graphs

abstract: Program dependence graphs are an important program representation technique for use in vectorization, parallelization and programming environments. We present a graph rewriting semantics for program dependence graphs and prove the equivalence between the program dependence graphs semantics and the operational semantics for programs. We then propose a framework for studying program transformations using program dependence graphs and a programming language calculus based on this rewriting semantics.


abstract: In this paper we present A Calculus of Higher Order Communicating Systems. This calculus considers sending and receiving processes to be as fundamental as nondeterminism and parallel composition.


title: How to Make ad-hoc Polymorphism Less ad-hoc

authors:
Philip Wadler
Stephen Blott

abstract: This paper presents type classes, a new approach to ad-hoc polymorphism. Type classes permit overloading of arithmetic operators such as multiplication, and generalise the “eqtype variables” of Standard ML. Type classes extend the Hindley/Milner polymorphic type system, and provide a new approach to issues that arise in object-oriented programming, bounded type quantification, and abstract data types. This paper provides an informal introduction to type classes, and defines them formally by means of type inference rules.


title: Moded Type Systems for Logic Programming

authors:
Katherine A. Yelick
Joseph L. Zachary

abstract: Most of the theoretical work on the semantics of logic programs assumes an interpreter that provides a complete resolution procedure. In contrast, for reasons of efficiency, most logic programming languages are built around incomplete procedures. This difference is rooted in Prolog, which evaluates resolvent trees in a depth-first rather than a breadth-first order. The gap is widened by some equational logic languages, which combine the incompleteness of depth-first evaluation with incomplete approximations to equational unification. Because of this gap, it is unsound to reason about logic programs using their declarative semantics. This in turn makes it difficult to develop abstraction mechanisms that can be used to partition a logic program into independently specifiable modules.


title: Explicit Substitutions

authors:
Martín Abadi
Luca Cardelli
Pierre-Louis Curien
Jean-Jacques Lévy

abstract: The λσ-calculus is a refinement of the λ-calculus where substitutions are manipulated explicitly. The λσ-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical λ-calculus and concrete implementations.


title: Program Transformation in the Presence of Errors

authors:
Alexander Aiken
John H. Williams
Edward L. Wimmers

abstract: Language designers and implementors have avoided specifying and preserving the meaning of programs that produce errors. This is apparently because being forced to preserve error behavior severely limits the scope of program optimization, even for correct programs. However, preserving error behavior is desirable for debugging, and error behavior must be preserved in any language that permits user-generated exceptions.


title: Implicative Formulae in the "Proofs as Computations" Analogy

authors:
Andrea Asperti
Gian-Luigi Ferrari
Roberto Gorrieri

abstract: In [As87] a correspondence between the subset of Linear Logic [Gi86] involving the conjunctive tensor product only and Place/Transition Petri Nets [Rei85] is established. In this correspondence, formulae are regarded as distributed states and provable sequents are computations in the net. Developing this idea, Martì-Oliet and Meseguer [MaM89] have suggested that all the other computations of Linear Logic, which do not have an immediate correspondence with Petri Nets, should be regarded as “gedanken” or idealized processes, providing a richer language for the specification and the study of properties of distributed computations. In this paper we apply this program to the fundamental connective of linear implication. We prove that the introduction of linear implication allows us to observe the net at a lower, more decentralized level of atomicity, where the preemption of each resource needed for the firing of a transition is represented as a separate move. We give a conservative theorem relating computations at different levels of abstraction. The categorical semantics establishes a tight correspondence among Petri nets, monoidal closed categories and tensor theories, reminiscent of the well known relation among functional languages, Cartesian closed categories and intuitionistic logic [LS86]. The identification of computations in the categorical model naturally suggests the generalisation of the notion of process [DMM89] at the lower level of atomicity.


title: Fairness and Hyperfairness in Multi-Party Interactions

authors:
Paul C. Attie
Nissim Francez
Orna Grumberg

abstract: In this paper, a new fairness notion is proposed for languages with multi-party interactions as the sole interprocess synchronization and communication primitive. The main advantage of this fairness notion is the elimination of starvation occurring solely due to race conditions (i.e., ordering of independent actions). Also, this is the first fairness notion for such languages which is fully-adequate with respect to the criteria presented in [AFK88]. The paper defines the notion, proves its properties, and presents examples of its usefulness.


title: The Chemical Abstract Machine

authors:
Gérard Berry
Gérard Boudol

abstract: We introduce a new kind of abstract machine based on the chemical metaphor used in the Γ language of Banâtre & al. States of a machine are chemical solutions where floating molecules can interact according to reaction rules. Solutions can be stratified by encapsulating subsolutions within membranes that force reactions to occur locally. We illustrate the use of this model by describing the operational semantics of the TCCS and CCS process calculi. We also show how to extract a higher-order concurrent λ-calculus out of the basic concepts of the chemical abstract machine.


title: A Relationship Between Abstract Interpretation and Projection Analysis

abstract: Abstract interpretation and projection analysis are two techniques for finding out information about lazy functional programs. Two typical uses of these techniques are speeding up sequential implementations, and the introduction of parallelism into parallel implementations.


title: Inheritance Is Not Subtyping

authors:
William R. Cook
Walter L. Hill
Peter S. Canning

abstract: In typed object-oriented languages the subtype relation is typically based on the inheritance hierarchy. This approach, however, leads either to insecure type-systems or to restrictions on inheritance that make it less flexible than untyped Smalltalk inheritance. We present a new typed model of inheritance that allows more of the flexibility of Smalltalk inheritance within a statically-typed system. Significant features of our analysis are the introduction of polymorphism into the typing of inheritance and the uniform application of inheritance to objects, classes and types. The resulting notion of type inheritance allows us to show that the type of an inherited object is an inherited type but not always a subtype.


title: Combining Generational and Conservative Garbage Collection: Framework and Implementations

authors:
Alan J. Demers
Mark D. Weiser
Barry Hayes
Hans-Juergen Boehm
Daniel G. Bobrow
Scott Shenker

abstract: Two key ideas in garbage collection are generational collection and conservative pointer-finding. Generational collection and conservative pointer-finding are hard to use together, because generational collection is usually expressed in terms of copying objects, while conservative pointer-finding precludes copying. We present a new framework for defining garbage collectors. When applied to generational collection, it generalizes the notion of younger/older to a partial order. It can describe traditional generational and conservative techniques, and lends itself to combining different techniques in novel ways. We study in particular two new garbage collectors inspired by this framework. Both these collectors use conservative pointer-finding. The first one is based on a rewrite of an existing trace-and-sweep collector to use one level of generation. The second one has a single parameter, which controls how objects are partitioned into generations: the value of this parameter can be changed dynamically with no overhead. We have implemented both collectors and present measurements of their performance in practice.


title: On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specifications

abstract: We present a static analysis method for determining aliasing and lifetime of dynamically allocated data in lexically scoped, higher-order, strict and polymorphic languages with first class continuations. The goal is validate program transformations that introduce imperative constructs such as destructive updatings, stack allocations and explicit deallocations in order to reduce the run-time memory management overhead. Our method is based on an operational model of higher order functional programs from which we construct statically computable abstractions using the abstract interpretation framework. Our method provides a solution to a problem left open [Hudak 86]: determining isolation of data in the case of higher order languages with structured data.


title: On Laziness and Optimality in Lambda Interpreters: Tools for Specification and Analysis

abstract: In this paper, we introduce a new formal system, $\Lambda CCL$, based on Curien's Categorical Combinators [Cur86a]. We show that $\Lambda CCL$ has properties that make it especially suitable for analysis and implementation of a wide range of $\lambda$-reduction schemes using shared environments, closures, or $\lambda$-terms. In particular, the term structure of $\Lamda CCL$ is very closely related to the structure of existing abstract machines for $\lambda$-reduction. $\Lambda CCL$ is powerful enough to mimic arbitrary (strong) reduction in the $\lambda$-calculus, yet in contrast to the systems in [Cur86a] it is also confluent (on ground terms).As an example of the practical utility of this formalism, we use it to specify a simple lazy interpreter for the $\lambda$-calculus, whose correctness follows trivially from the properties of $\LambdaCCL$. We then describe a labeled variant of $\Lambda CCL, \Lambda CCL^{L}$, which can be used as a tool to determine the degree of "laziness" possessed by various $\lambda$-reduction schemes. In particular, $\Lambda CCL^{L}$ is applied to the problem of optimal reduction in the $\lambda$-calculus. A reduction scheme for the $\lambda$-calculus is optimal if the number of redex contractions that must be performed in the course of reducing any $\lambda$-term to a normal form (if one exists) is guaranteed to be minimal. Results of Levy [Lev78, Lev80] showed that for a natural class of reduction strategies allowing shared redexes, optimal reductions were, at least in principle, possible. He conjectured that an optimal reduction strategy might be realized in practice using shared closures and environments as well as shared $\lambda$-terms. However, using $\Lambda CCL^{L}$, we show that the sharing allowed by environments and closures in $\Lambda CCL$ as implemented using standard term graph-rewriting techniques [BvEG$^{+}$87] is insufficient to implement optimal reduction.


title: A Type System for Smalltalk

authors:
Justin O. Graver
Ralph E. Johnson

abstract: This paper describes a type system for Smalltalk that is type-safe, that allows most Smalltalk programs to be type-checked, and that can be used as the basis of an optimizing compiler.


title: A Formulae-as-Types Notion of Control

abstract: The programming language Scheme contains the control construct call/cc that allows access to the current continuation (the current control context). This, in effect, provides Scheme with first-class labels and jumps. We show that the well-known formulae-as-types correspondence, which relates a constructive proof of a formula α to a program of type α, can be extended to a typed Idealized Scheme. What is surprising about this correspondence is that it relates classical proofs to typed programs. The existence of computationally interesting “classical programs” —programs of type α, where α holds classically, but not constructively — is illustrated by the definition of conjunctively, disjunctive, and existential types using standard classical definitions. We also prove that all evaluations of typed terms in Idealized Scheme are finite.


title: Relating Total and Partial Correctness Interpretations of Non-Deterministic Programs

abstract: The purpose of this paper is to discuss the relationship between the interpretations of non-deterministic programs using the upper (total correctness) powerdomain on the one hand and the lower (partial correctness) powerdomain on the other. It is shown that there is a close semantic relationship between these two interpretations which suggests the formulation of a new operator called the mixed powerdomain. It is shown that the mixed powerdomain has many pleasing domain-theoretic and algebraic properties. The mixed powerdomain is closely related to new powerdomains which have been recently investigated as mathematical models of partial information in databases. Some of the basic intuitions captured by such structures may have uses for the specification of non-deterministic computations. The paper includes a sample non-deterministic programming language and a semantics using the mixed powerdomain.


title: Higher-Order Modules and the Phase Distinction

authors:
Robert Harper
John C. Mitchell
Eugenio Moggi

abstract: In earlier work, we used a typed function calculus, XML, with dependent types to analyze several aspects of the Standard ML type system. In this paper, we introduce a refinement of XML with a clear compile-time/run-time phase distinction, and a direct compile-time type checking algorithm. The calculus uses a finer separation of types into universes than XML and enforces the phase distinction using a nonstandard equational theory for module and signature expressions. While unusual from a type-theoretic point of view, the nonstandard equational theory arises naturally from the well-known Grothendieck construction on an indexed category.


title: A Finite Presentation Theorem for Approximating Logic Programs

authors:
Nevin Heintze
Joxan Jaffar

abstract: The notion of Cartesian closure on a set of unifiers has been used to define approximations of the least models of logic programs. Such approximations, often called types, are not known to be recursive. In this paper, we use Cartesian closure to define a similar, but more accurate, approximation. The main result proves that our approximation is not only recursive, but that it can be finitely represented in the form of a cyclic term graph. This explicit representation can be used as a starting point for logic program analyzers.


title: Interaction Nets

abstract: We propose a new kind of programming language, with the following features:a simple graph rewriting semantics,a complete symmetry between constructors and destructors,a type discipline for deterministic and deadlock-free (microscopic) parallelism.Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a naive and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.


title: An Algorithm for Optimal Lambda Calculus Reduction

abstract: We present an algorithm for lambda expression reduction that avoids any copying that could later cause duplication of work. It is optimal in the sense defined by Lévy. The basis of the algorithm is a graphical representation of the kinds of commonality that can arise from substitutions; the idea can be adapted to represent other kinds of expressions besides lambda expressions. The algorithm is also well suited to parallel implementations, consisting of a fixed set of local graph rewrite rules.


title: Deciding ML Typability is Complete for Deterministic Exponential Time

abstract: A well known but incorrect piece of functional programming folklore is that ML expressions can be efficiently typed in polynomial time. In probing the truth of that folklore, various researchers, including Wand, Buneman, Kanellakis, and Mitchell, constructed simple counterexamples consisting of typable ML programs having length n, with principal types having Ω(2cn) distinct type variables and length Ω(22cn). When the types associated with these ML constructions were represented as directed acyclic graphs, their sizes grew as Ω(2cn). The folklore was even more strongly contradicted by the recent result of Kanellakis and Mitchell that simply deciding whether or not an ML expression is typable is PSPACE-hard.


title: An Efficient Hybrid Algorithm for Incremental Data Flow Analysis

authors:
Thomas J. Marlowe
Barbara G. Ryder

abstract: Our exhaustive and incremental hybrid data flow analysis algorithms, based on iteration and elimination techniques, are designed for incremental update of a wide variety of monotone data flow problems in response to source program changes. Unlike previous incremental iterative methods, this incremental algorithm efficiently computes precise and correct solutions. We give theoretical results on the imprecision of restarting iteration for incremental update by fixed point iteration which provided motivation for our algorithm design. Described intuitively, the main algorithm idea is to factor the data flow solution on strong connected components of the flow graph into local and external parts, solving for the local parts by iteration and propagating these effects on the condensation of the flow graph to obtain the entire data flow solution. The incremental hybrid algorithm re-performs those algorithm steps affected by the program changes.


title: Toward a Typed Foundation for Method Specialization and Inheritance

abstract: This paper discusses the phenomenon of method specialization in object-oriented programming languages. A typed function calculus of objects and classes is presented, featuring method specialization when methods are added or redefined. The soundness of the typing rules (without subtyping) is suggested by a translation into a more traditional calculus with recursively-defined record types. However, semantic questions regarding the subtype relation on classes remain open.


title: Computable processes

abstract: In this paper we study concurrent, asynchronous processes and functions on them which can be programmed using the (full) unfair or the fair merge operations. The main result is a normal form theorem for these (relatively) “computable process functions” which implies that although they can be very complex when viewed as classical set-functions, they are all “loosely implementable” in the sense of Park [7]. We also announce a variation and a substantial strengthening of the main “transfer principle” of [4] which have applications to the semantics and logic of programming languages with interactive (deterministic) or concurrent (non-deterministic) constructs.


title: Scheduling Time-Critical Instructions on RISC Machines

authors:
Krishna V. Palem
Barbara B. Simons

abstract: We present a polynomial time algorithm for constructing a minimum completion time schedule of instructions from a basic block on RISC machines such as the Sun SPARC, the IBM 801, the Berkeley RISC machine, and the HP Precision Architecture. Our algorithm can be used as a heuristic for RISC processors with longer pipelines, for which there is no known optimal algorithm. Our algorithm can also handle time-critical instructions, which are instructions that have to be completed by a specific time. Time-critical instructions occur in some real-time computations, and can also be used to make shared resources such as registers quickly available for reuse. We also prove that in the absence of time-critical constraints, a greedy scheduling algorithm always produces a schedule for a target machine with multiple identical pipelines that has a length less than twice that of an optimal schedule. The behavior of the heuristic is of interest because, as we show, the instruction scheduling problem becomes NP-hard for arbitrary length pipelines, even when the basic block of code being input consists of only several independent streams of straightline code, and there are no time-critical constraints, Finally, we prove that the problem becomes NP-hard even for small pipelines, no time-critical constraints, and input of several independent streams of straightline code if either there is only a single register or if no two instructions are allowed to complete simultaneously because of some shared resource such as a bus


title: Parallelism in Logic Programs

abstract: Article Free Access Share on Parallelism in logic programs Author: Raghu Ramakrishnan Computer Sciences Department, University of Wisconsin-Madison, WI Computer Sciences Department, University of Wisconsin-Madison, WIView Profile Authors Info & Claims POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesDecember 1989 Pages 246–260https://doi.org/10.1145/96709.96734Online:01 December 1989Publication History 1citation225DownloadsMetricsTotal Citations1Total Downloads225Last 12 Months10Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Automata-Driven Indexing of Prolog Clauses

authors:
R. Ramesh
I. V. Ramakrishnan
David Scott Warren

abstract: Indexing Prolog clauses is an important optimization step that reduces the number of clauses on which unification will be performed and can avoid the pushing of a choice point. It is quite desirable to increase the number of functors used in indexing as this can considerably reduce the size of the filtered set. However this can cause an enormous increase in running time if indexing is done naively. This paper describes a new technique for indexing that utilizes all the functors in a clause-head. More importantly, in spite of using all the functors, this technique is still able to quickly select relevant clause-heads at run time. This is made possible primarily by a finite-state automaton that guides the indexing process. The automaton is constructed at compile time by preprocessing all the clause-heads.


title: Safe Run-time Overloading

abstract: We present a functional language featuring a form of dynamic overloading akin to message passing in object oriented languages. We give a dynamic semantics describing a non-deterministic evaluation, as well as a type discipline (static semantics) supporting type inference. The type system ensures that a well-typed program has a correct execution, unique up to a semantic equivalence relation, and allows this execution to proceed deterministically, while resolving overloading at run-time.


title: On Oraclizable Networks and Kahn's Principle

abstract: In this paper we investigate generalizations of Kahn's principle to nondeterministic dataflow networks. Specifically, we show that for the class of "oraclizable" networks a semantic model in which networks are represented by certain sets of continuous functions is fully abstract and has the fixed-point property. We go on to show that the oraclizable networks are the largest class representable by this model, and are a proper superclass of the networks implementable with the infinity fair merge primitive. Finally, we use this characterization to show that infinity fair merge networks and oraclizable networks are proper subclasses of the networks with Egli-Milner monotone input-output relations.


title: Concurrent Constraint Programming

authors:
Vijay A. Saraswat
Martin C. Rinard

abstract: This paper presents a new and very rich class of (con-current) programming languages, based on the notion of comput.ing with parhal information, and the con-commitant notions of consistency and entailment. ’ In this framework, computation emerges from the inter-action of concurrently executing agents that communi-cate by placing, checking and instantiating constraints on shared variables. Such a view of computation is in-teresting in the context of programming languages be-cause of the ability to represent and manipulate partial information about the domain of discourse, in the con-text of concurrency because of the use of constraints for communication and control, and in the context of AI because of the availability of simple yet powerful mechanisms for controlling inference, and the promise that very rich representational/programming languages, sharing the same set of abstract properties, may be pos-sible. To reflect this view of computation, [Sar89] develops the cc family of languages. We present here one mem-ber of the family, CC(.L,+) (pronounced “cc with Ask and Choose”) which provides the basic operations of blocking Ask and atomic Tell and an algebra of be-haviors closed under prefixing, indeterministic choice, interleaving, and hiding, and provides a mutual recur-sion operator. cc(.L,-t) is (intentionally!) very similar to Milner’s CCS, but for the radically different under-lying concept of communication, which, in fact, pro-’ The class is founded on the notion of “constraint logic pro-gramming ” [JL87,Mah87], fundamentally generalizes concurrent logic programming, and is the subject of the first author’s disser-tation [Sar89], on which this paper is substantially based.


title: Small Domains Spell Fast Strictness Analysis

authors:
R. C. Sekar
Shaunak Pawagi
I. V. Ramakrishnan

abstract: Use of strictness analysis in parallel evaluation and optimization of lazy functional languages is well known. The first formal treatment of strictness analysis appeared in Mycroft's seminal work which however dealt only with flat domains. Unlike flat domains, strictness analysis on non-flat domains involves determining how a function transforms a demand (degree of strictness) on its output into a demand on its arguments. Solutions to this problem in its full generality require large domains and appear both complex and expensive to implement. However, only two kinds of demands arise naturally in lazy normalization of terms, viz., e-demand (normal form needed) and d-demand (root stable or head normal form needed). Based on this observation, we identify three useful forms of strictness for non-flat domains - ee, dd and de. Each of these three forms of strictness play an important role in evaluation of functional programs. Specifically, ee strictness is used for transforming call-by-need to call-by-value and dd strictness is useful in repairing violations of strong sequentiality of equational programs as well as in a critical optimization step used in rewriting implementations of such languages. We present intuitively simple methods to compute them. Our methods are computationally efficient as they are based on small domains (1 point for ee and dd and 2 points for de). They are powerful enough to extract all useful strictness information in practice and are general enough to handle functions defined by rewrite rules. We are able to reason about all user defined data types within a single framework and also handle polymorphism.


title: On the Relations Computable by a Class of Concurrent Automata

abstract: We consider monotone input/output automata, which model a usefully large class of dataflow networks of indeterminate (or nonfunctional) processes. We obtain a characterization of the relations computable by these automata, which states that a relation R : X ! 2 Y (viewed as a "nondeterministic function") is the input /output relation of an automaton iff there exists a certain kind of Scott domain D, a continuous function F : X ! [D ! Y ] and a continuous function G : X ! P(D), such that R(x) = F (x) y (G(x)) for all inputs x 2 X. Here P denotes a certain powerdomain operator, and y denotes the pointwise extension to the powerdomain of a function on the underlying domain. An attractive feature of this result is that it specializes to two subclasses of automata, determinate automata, for which G is single-valued, and semi-determinate automata, for which G is a constant function. A corollary of the latter result is the impossibility of implementing "angelic merge" by a network of de...


title: Making Asynchronous Parallelism Safe for the World

abstract: We need a programming model that combines the advantages of the synchronous and asynchronous parallel styles. Synchronous programs are determinate (thus easier to reason about) and avoid synchronization overheads. Asynchronous programs are more flexible and handle conditionals more efficiently.Here we propose a programming model with the benefits of both styles. We allow asynchronous threads of control but restrict shared-memory accesses and other side effects so as to prevent the behavior of the program from depending on any accidents of execution order that can arise from the indeterminacy of the asynchronous process model.These restrictions may be enforced either dynamically (at run time) or statically (at compile time). In this paper we concentrate on dynamic enforcement, and exhibit an implementation of a parallel dialect of Scheme based on these ideas. A single successful execution of a parallel program in this model constitutes a proof that the program is free of race conditions (for that particular set of input data).We also speculate on a design for a programming language using static enforcement. The notion of distinctness is important to proofs of noninterference. An appropriately designed programming language must support such concepts as “all the elements of this array are distinct,” perhaps through its type system.This parallel programming model does not support all styles of parallel programming, but we argue that it can support a large class of interesting algorithms with considerably greater efficiency (in some cases) than a strict SIMD approach and considerably greater safety (in all cases) than a full-blown MIMD approach.


title: Quasi-Static Typing

abstract: We present a new approach to dynamic typing in a static framework. Our main innovation is the use of structural subtyping for dynamic types based on the idea that possible dynamic typing as a property should be inherited by objects of all types. Two properties of our system set it apart from existing systems which combine static and dynamic typing: all tagging and checking takes place via implicit coercions, and the semantics of dynamic typing is representation independent. The latter property leads to a significant increase in expressive power—for instance it allows us to define a general call-by-value fixpoint operator.The resulting system—which we call quasi-static typing—is a seamless merger of static and dynamic typing. The system divides programs into three categories: well-typed, ill-typed and ambivalent programs. Ill-typed programs contain expressions that are guaranteed to go wrong. Run-time checking is limited to doubtful function applications in ambivalent programs. Conceptually, quasi-static typing takes place in an unusual two-phase process—a first phase infers types and coercions and a second plausibility checking phase identifies ill-typed programs. The typing rules allow minimal typing judgements and plausibility checking can be characterized as simplification via a canonical set of rewrite rules. The two phase process can therefore be implemented with a one pass algorithm.


title: A Logical View of Composition and Refinement

authors:
Martín Abadi
Gordon D. Plotkin

abstract: We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition and refinement rules, and a framework for the use of the modular specification methods that these rules underpin. The two logics arise naturally from extant specification approaches; one of the logics is intuitionistic, while the other one is linear.


title: A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions

authors:
Samson Abramsky
Thomas P. Jensen

abstract: This paper defines the categorical notions of relators and transformations and shows that these concepts enable us to give a semantics for polymorphic, higher order functional programs.We demonstrate the pertinence of this semantics to the analysis of polymorphic programs by proving that strictness analysis is a polymorphic invariant.


title: Static Type Inference in a Dynamically Typed Language

authors:
Alexander Aiken
Brian R. Murphy

abstract: We present a type inference system for FL based on an operational, rather than a denotational, formulation of types. The essential elements of the system are a type language based on regular trees and a type inference logic that implements an abstract interpretation of the operational semantics of FL. We use a non-standard approach to type inference because our requirements---using type information in the optimization of functional programs---differ substantially from those of other type systems. 1 Introduction Compilers derive at least two benefits from static type inference: the ability to detect and report potential run-time errors at compile-time, and the use of type information in program optimization. Traditionally, type systems have emphasized the detection of type errors. Statically typed functional languages such as Haskell [HWA*88] and ML [HMT89] include type constraints as part of the language definition, making some type inference necessary to ensure that type constraints ...


title: Subtyping Recursive Types

authors:
Roberto M. Amadio
Luca Cardelli

abstract: Article Free Access Share on Subtyping recursive types Authors: Roberto M. Amadio LIENS, Ecole Normale Supérieure, Paris LIENS, Ecole Normale Supérieure, ParisView Profile , Luca Cardelli DEC, Systems Research Center DEC, Systems Research CenterView Profile Authors Info & Claims POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1991 Pages 104–118https://doi.org/10.1145/99583.99600Published:03 January 1991Publication History 58citation352DownloadsMetricsTotal Citations58Total Downloads352Last 12 Months13Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: "Look Ma, No Hashing, And No Arrays Neither"

authors:
Jiazhen Cai
Robert Paige

abstract: It is generally assumed that hashing is essential to many algorithms related to efficient compilation; e.g., symbol table formation and maintenance, grammar manipulation, basic block optimization, and global optimization.This paper questions this assumption, and initiates development of an efficient alternative compiler methodology without hashing or sorting.Underlying this methodology are several generic algorithmic tools, among which special importance is given to Multiset Discrimination, which partitions a multiset into blocks of duplicate elements.We show how multiset discrimination, together with other tools, can be tailored to rid compilation of hashing without loss in asymptotic performance.Because of the simplicity of these tools, our results maybe of practical as well as theoretical interest.The various applications presented culminate with a new algorithm to solve iterated strength reduction folded with useless code elimination that runs in worst case asymptotic time and auxiliary space linear in the maximum text length of the initial and optimized programs.1. Introduction.with linear search time and a hash table.They also pro-An important practical and theoretical question in Computer Science is whether there are algorithms whose worst case performance can match the expected performance of solutions that utilize hashing.In the context of this broader question, we initiate an investigation of efficient compilation without hashing and, consequently, raise some doubts about the prevailing view that hashing (e.g., universal hashing [5]) is essential to the various 2. The research of this author was partiatly


title: Automatic Construction of Sparse Data Flow Evaluation Graphs

authors:
Jong-Deok Choi
Ron Cytron
Jeanne Ferrante

abstract: In this paper, we present an algorithm that con-structs sparse evaluation graphs for forward or backward monotone data flow problems. The sparse graph combines information as early as possible, yet directly connects nodes that generate and use information. This allows problems from the large, general class of monotone data flow problems to err joy the advantages of solutions based on Static Single Assignment (SSA) form. 1


title: Macros That Work

authors:
William D. Clinger
Jonathan Rees

abstract: Article Macros that work Share on Authors: William Clinger Department of Computer Science, University of Oregon Department of Computer Science, University of OregonView Profile , Jonathan Rees Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MAView Profile Authors Info & Claims POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1991 Pages 155–162https://doi.org/10.1145/99583.99607Online:03 January 1991Publication History 102citation1,489DownloadsMetricsTotal Citations102Total Downloads1,489Last 12 Months27Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access