title: Incremental Data Flow Analysis

abstract: In this paper we present ACINCF and ACINCB, incremental update algorithms for forward and backward data flow problems, which are based on a linear equations model of Allen/Cocke interval analysis [Allen 77, Ryder 82a]. We have studied their performance on a robust structured programming language L. Given a set of localized program changes in a program in L, we can identify a priori the nodes in its flow graph whose corresponding data flow equations will be affected by the changes. We can characterize these affected nodes by their corresponding program structures and their relation to the original change sites.


venue: popl

title: Mechanisms for Compile-Time Enforcement of Security

abstract: This paper discusses features of a secure systems programming language designed and implemented at IBM's Watson Research Lab. Two features of the language design were instrumental in permitting security to be enforced with minimum run-time cost: (1) Language constructs (e.g. pointer variables) which could result in aliasing were removed from the programmer's direct control and replaced by higher level primitive types; and (2) traditional strong type checking was enhanced with typestate checking, a new mechanism in which the compiler guarantees that for all execution paths, the sequence of operations on each variable obeys a finite state grammar associated with that variable's type. Examples are given to illustrate the application of these mechanisms.


title: Loops in Combinator-Based Compilers

abstract: In our paper [Wand 82a], we introduced a paradigm for compilation based on combinators. A program from a source language is translated (via a semantic definition) to trees of combinators; the tree is simplified (via associative and distributive laws) to a linear, assembly-language-like format: the compiler writer's virtual machine operates by simulating a reduction sequence of the simplified tree. The correctness of these transformations follows from general results about the λ-calculus. The code produced by such n generator is always tree-like. In this paper, the method is extended to produce target code with explicit loops. This is done by re-introducing variables into the terms of the target language in a restricted way, along with a structured binding operator.


title: Summarizing Graphs by Regular Expressions

abstract: This paper shows how to rapidly determine the path relationships between k different elements of a graph (of the type primarily resulting from programs) in time proportional to k log k. Given the path relations between elements u,v, and w, it is easy to answer questions like "is there a path from u to w?" and "is there a path from u to w which does not go through v?" (The elements can be either nodes or edges.)This algorithm can be used in a wide variety of contexts. For example, in order to prove that whenever control reaches a point p, the last assignment of a value to a variable, v, has always been of the form v := c, where c is a certain constant, it is only necessary to know the path relations between the point p and all assignments to that variable.Ordinarily one is interested in the possible points, where a variable was assigned its current value (definition points), and at the points at which that value is used. Previously, all flow analysis algorithms would compute the definition points of all variables at all nodes in the graph, despite the fact that any given node may use only one of those variables.This algorithm may also be a generally useful graph algorithm. It can compute transitive closure more rapidly than the standard algorithm using the current best matrix multiplication algorithm on the kinds of graphs resulting from programs. The algorithm proceeds by preprocessing the graph, creating tables that can be used later to rapidly determine flow relationships between any sections of the program. In addition, small changes to the graph need only result in small changes to the tables. The algorithm is therefore suitable for incremental analysis.


title: On the Unification of Data and Program Abstraction in Ada

abstract: Ada is rich in the variety of its abstraction mechanisms. It has both a data abstraction mechanism (packages with private data types) that supports a functional programming style and a program abstraction mechanism (generic program units) that supports an object-oriented program style. Tradeoffs between data and program abstraction are examined and it is pointed out that Ada discourages program abstraction because program units are not first-class objects. It is shown how program units could be made into first-class objects by introducing closures as values for functions and records with function components as values for packages. Further unification by allowing types to be first-class objects conflicts with the requirement of compile-time type invariance. The relaxation of this requirement in a manner that preserves type consistency is examined and leads to a notion of value for types as tuples of operations. It is suggested in the conclusion that our understanding of abstraction for object-oriented languages and of other language design, implementation, and environment issues will have progressed sufficiently by 1985 to warrant the design of a successor to Ada by the late 1980s.


title: Constraining-Unification and the Programming Language Unicorn

abstract: Up to this point direct implementations of axiomatic or equational specifications have been limited because the implementation mechanisms used are incapable of capturing the full semantics of the specifications. The programming language Unicorn was designed and implemented with the intention of exploring the full potential of programming with equations. Unicorn introduces a new language mechanism, called constraining-unification. When coupled with semantic unification, constraining-unification closely models the semantics of equational specifications thereby allowing for the implementation of a wider class of specifications. Unlike the language mechanisms of rewrite-rule and logic programming, constraining-unification is free of order dependencies. The same results are produced regardless of the order in which the axioms are stated. The use of viewpoints contributes to the flexibility of the Unicorn language. Preconditions for partial operations can be specified without added machinery.


title: Efficient Implementation of the Smalltalk-80 System

authors:
L. Peter Deutsch
Allan M. Schiffman

abstract: The Smalltalk-80* programming language includes dynamic storage allocation, full upward funargs, and universally polymorphic procedures; the Smalltalk-80 programming system features interactive execution with incremental compilation, and implementation portability. These features of modern programming systems are among the most difficult to implement efficiently, even individually. A new implementation of the Smalltalk-80 system, hosted on a small microprocessor-based computer, achieves high performance while retaining complete (object code) compatibility with existing implementations. This paper discusses the most significant optimization techniques developed over the course of the project, many of which are applicable to other languages. The key idea is to represent certain runtime state (both code and data) in more than one form, and to convert between forms when needed.


title: Generalized Fair Termination

authors:
Nissim Francez
Dexter Kozen

abstract: We present a generalization of the known fairness and equifairness notions, called @@@@-fairness, in three versions: unconditional, weak and strong. For each such version, we introduce a proof rule for the @@@@-fair termination induced by it, using well-foundedness and countable ordinals. Each such rule is proved to be sound and semantically complete. We suggest directions for further research.


title: On Relative Completeness of Programming Logics

abstract: In this paper a generalization of a certain Lipton's theorem (see Lipton [5]) is presented. Namely, we show that for a wide class of programming languages the following holds: the set of all partial correctness assertions true in an expressive interpretation I is uniformly decidable (in I) in the theory of I iff the halting problem is decidable for finite interpretations. In the effect we show that such limitations as effectiveness or Herbrand definability of interpretation (they are relevant in the previous proofs) can be removed in the case of partial correctness.


title: A Good Hoare Axiom System for an Algol-like Language

abstract: Clarke has shown that it is impossible to obtain a relatively complete axiomatization of a block-structured programming language if it has features such as static scope, recursive procedure calls with procedure parameters, and global variables, provided that we take first-order logic as the underlying assertion language [Cl]. We show that if we take a more powerful assertion language, and hence a more powerful notion of expressiveness, such a complete axiomatization is possible. The crucial point is that we need to be able to express weakest preconditions of commands with free procedure parameters. The axioms presented here are natural and reflect the syntax of the programming language. Such an axiom system provides a tool for understanding how to reason about languages with powerful control features.


title: The Semantics of Local Storage, or What Makes the Free-List Free?

authors:
Joseph Y. Halpern
Albert R. Meyer
Boris A. Trakhtenbrot

abstract: Denotational semantics for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing) is given by translating programs into an appropriately typed l-calculus. Procedures are entirely explained at a purely functional level - independent of the interpretation of program constructs - by continuous models for l-calculus. However, the usual (cpo) models are not adequate to model local storage allocation for blocks because storage overflow presents an apparent discontinuity. New domains of store models are offered to solve this problem.


title: Implementation of an Interpreter for Abstract Equations

authors:
Christoph M. Hoffmann
Michael J. O'Donnell

abstract: This paper summarizes a project, introduced in [HO79, HO82b], whose goal is the implementation of a useful interpreter for abstract equations that is absolutely faithful to the logical semantics of equations. The Interpreter was first distributed to Berkeley UNIX VAX sites in May, 1983. The main novelties of the interpreter are


title: A Combinator-Based Compiler for a Functional Language

authors:
Paul Hudak
David A. Kranz

abstract: Article Free Access Share on A combinator-based compiler for a functional language Authors: Paul Hudak Yale University, Department of Computer Science Yale University, Department of Computer ScienceView Profile , David Kranz Yale University, Department of Computer Science Yale University, Department of Computer ScienceView Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 122–132https://doi.org/10.1145/800017.800523Online:15 January 1984Publication History 24citation0DownloadsMetricsTotal Citations24Total Downloads0Last 12 Months0Last 6 weeks0 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: Applicative Programming and Digital Design

abstract: This paper adapts applicative programming techniques to the synthesis of mynchronaua system descriptions.It presents a unifying perspective on hardware and software engineering and shows that a functional design paradigm is suitable in both realms.Established techniques for program synthesis are extended to yield hardware descriptions.This work stems from research in general programming methods for systems.Synchronous systems are a valuable special case.They are a preferred basis for hardware design: logical synchrony makes circuits easier to conceptualize, and physical synchrony makes them easier to test.Applicative notation is well suited to the description of digital circuits because it has an immediate interpretation in terms of wiring.Digital circuits are a reasonable target for synthesis because they are functional in character.The design approach is conventional: a circuit is viewed as a sequential control algorithm acting on an architecture [17].This should sound familiar to programmers who view their product as an algorithm acting on an abstract type.An engineer starts with an abstractly descriptive specification and derives a concretely descriptive realization.These notations should be suited not only to what they describe but also to each other.


title: Completion of a Set of Rules Modulo a Set of Equations

authors:
Jean-Pierre Jouannaud
Hélène Kirchner

abstract: Article Completion of a set of rules modulo a set of equations Share on Authors: Jean-Pierre Jouannaud CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE) CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)View Profile , Helene Kirchner CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE) CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)View Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 83–92https://doi.org/10.1145/800017.800519Online:15 January 1984Publication History 41citation373DownloadsMetricsTotal Citations41Total Downloads373Last 12 Months8Last 6 weeks0 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: An Ideal Model for Recursive Polymorphic Types

authors:
David B. MacQueen
Gordon D. Plotkin
Ravi Sethi

abstract: Article Free Access Share on An ideal model for recursive polymorphic types Authors: David MacQueen Bell Laboratories, Murray Hill, New Jersey Bell Laboratories, Murray Hill, New JerseyView Profile , Gordon Plotkin Department of Computer Science, University of Edinburgh, Edinburgh EH9 3J2 Department of Computer Science, University of Edinburgh, Edinburgh EH9 3J2View Profile , Ravi Sethi Bell Laboratories, Murray Hill, New Jersey Bell Laboratories, Murray Hill, New JerseyView Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 165–174https://doi.org/10.1145/800017.800528Online:15 January 1984Publication History 79citation712DownloadsMetricsTotal Citations79Total Downloads712Last 12 Months48Last 6 weeks7 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: Direct Implementation of Compiler Specifications or the Pascal P-code Compiler Revisited

authors:
Don Milos
Uwe F. Pleban
George Loegel

abstract: We have developed a complete formal specification of the translation semantics of the Pascal P-compiler. The specification is written as a semantic grammar (a variant of extended attribute grammars), and has been extensively tested and debugged with the aid of Lawrence Paulson's experimental semantics processor. The translation semantics models the operational aspects of compilation in detail. It is one-pass, embodying static semantic checking, address assignment, code generation, and a certain amount of code improvement. Our paper describes the development history of the project, compares the new compiler with the existing P-compiler, and discusses our positive experience with semantic grammars and Paulson's system.


title: Static Inference of Properties of Applicative Programs

authors:
Prateek Mishra
Robert M. Keller

abstract: An applicative program denotes a function mapping values from some domain to some range. Abstract interpretation of applicative programs involves using the standard denotation to describe an abstract function from a “simplified” domain to a “simplified” range, such that computation of the abstract function is effective and yields some information, such as type information, about the standard denotation. We develop a general framework for a restricted class of abstract interpretations that deal with non-strict functions defined on non-flat domains. As a consequence, we can develop inference schemes for a large and useful class of functional programs, including functions defined on streams. We describe several practical problems and solve them using abstract interpretation. These include inferring minor signatures and relevant clauses of functions, which have arisen out of our work on a strongly-typed applicative language.


title: Coercion and Type Inference

abstract: A simple semantic model of automatic coercion is proposed. This model is used to explain four rules for inferring polymorphic types and providing automatic coercions between types. With the addition of a fifth rule, the rules become semantically complete but the set of types associated with an expression may be undecidable. An efficient type checking algorithm based on the first four rules is presented. The algorithm is guaranteed to find a type whenever a type can be deduced using the four inference rules. The type checking algorithm may be modified so that calls to type conversion functions are inserted at compile time.


title: A Less Dynamic Memory Allocation Scheme for Algol-like Languages

abstract: The conventional storage allocation scheme for block structured languages requires the allocation of stack space and the building of a display with each procedure call. This paper describes a technique for analyzing the call graph of a program in a block structured language that makes it possible to eliminate these operations from many call sequences, even in the presence of recursion.


title: Efficient Applicative Data Types

abstract: Article Efficient applicative data types Share on Author: Eugene W. Myers Department of Computer Science, The University of Arizona, Tucson, Arizona Department of Computer Science, The University of Arizona, Tucson, ArizonaView Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 66–75https://doi.org/10.1145/800017.800517Online:15 January 1984Publication History 46citation450DownloadsMetricsTotal Citations46Total Downloads450Last 12 Months18Last 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 SiteGet Access


title: Editing by Example

abstract: An editing by example system is an automatic program synthesis facility embedded in a text editor that can be used to solve repetitive text editing problems. The user provides the editor with a few examples of a text transformation. The system analyzes the examples and generalizes them into a program that can perform the transformation to the rest of the user's text.


title: Grids: A New Program Structuring Mechanism Based on Layered Graphs

abstract: Article Grids: A new program structuring mechanism based on layered graphs Share on Author: Harold L. Ossher Computer Science Department, Stanford University, Stanford, CA Computer Science Department, Stanford University, Stanford, CAView Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 11–22https://doi.org/10.1145/800017.800512Online:15 January 1984Publication History 16citation269DownloadsMetricsTotal Citations16Total Downloads269Last 12 Months5Last 6 weeks0 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: The Global Storage Needs of a Subcomputation

authors:
Jean-Claude Raoult
Ravi Sethi

abstract: A defining characteristic of “functional” specifications is the absence of assignments: updates of tables and data structures are expressed by giving the relationship between the new and old values. An obvious implementation allocates separate space for new and old values and may consume a lot of storage. However, even when updates of attributes like symbol tables are expressed functionally, we would like to avoid making copies of the symbol table during attribute evaluation. In other words, if possible, the implementation should have a single global copy of the table that is updated using assignments. Since the value of the global copy changes during computation, the order of evaluation has to be chosen carefully. In this paper, we partition attributes into classes, the problem being to determine if there exists an evaluation order that allows each class to share a global storage area. The solution extends to handle symbol tables for block structured languages.


title: Interactive Proof Checking

authors:
Thomas W. Reps
Bowen Alpern

abstract: Knowledge of logical inference rules allows a specialized proof editor to provide a user with feedback about errors in a proof under development. Providing such feedback involves checking a collection of constraints on the strings of the proof language. Because attribute grammars allow such constraints to be expressed in a modular, declarative fashion, they are a suitable underlying formalism for a proof-checking editor. This paper discusses how an attribute grammar can be used in an editor for partial-correctness program proofs in Hoare-style logic, where verification conditions are proved using the sequent calculus.


title: Treat - An Applicative Code Generator

authors:
Jerald S. Schwarz
Dean Rubine

abstract: Treat is a special purpose language for use in compiler writing. A Treat program translates a graph into c-trees (the intermediate language of the pcc compiler) and uses the back end of the C compiler to generate code. Treat has been developed specifically for use in an AdaTM compiler. A Treat program consists of applicative transformation rules. Treat's distinctive aspects include triggering transformations during pattern matching, a context mechanism for dynamic binding and assignment in a language with lazy evaluation.


title: Systems Programming in Concurrent Prolog

abstract: Concurrent Prolog [28] combines the logic programming computation model with guarded-command indeterminacy and dataflow synchronization. It will form the basis of the Kernel Language [21] of the Parallel Inference Machine [36], planned by Japan's Fifth Generation Computers Project. This paper explores the feasibility of programming such a machine solely in Concurrent Prolog (in the absence of a lower-level programming language), by implementing in it a representative collection of systems programming problems.


title: Temporal Verification of Carrier-Sense Local Area Network Protocols

authors:
Dennis E. Shasha
Amir Pnueli
W. Ewald

abstract: We examine local area network protocols and verify the correctness of two representative algorithms using temporal logic. We introduce an interval temporal logic that allows us to make assertions of the form “in the next k units, X holds.” This logic encodes intuitive arguments about contention protocols quite directly. We present two proofs of an Ethernet-like contention protocol, one using the interval temporal logic and one using classical temporal logic. We also verify a contention-free protocol using an invariant that seems to have wide applicability for such protocols.


title: Paragon: Novel Uses of Type Hierarchies for Data Abstraction

abstract: Article Free Access Share on Paragon: Novel uses of type hierarchies for data abstraction Author: Mark Sherman Department of Math. and Computer Science, Dartmouth College, Hanover, NH Department of Math. and Computer Science, Dartmouth College, Hanover, NHView Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 208–217https://doi.org/10.1145/800017.800532Published:15 January 1984Publication History 2citation195DownloadsMetricsTotal Citations2Total Downloads195Last 12 Months12Last 6 weeks0 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: Reflection and Semantics in Lisp


title: Pattern Driven Lazy Reduction: A Unifying Evaluation Mechanism for Functional and Logic Programs

authors:
P. A. Subrahmanyam
Jia-Huai You

abstract: A novel lazy evaluation mechanism, pattern-driven lazy reduction, is developed that serves as a unifying evaluation mechanism for both functional and logic programs. The reduction of a function call can be viewed as “semantically” unifying the function call with the left hand side of a defining equation, and applying the unifier to the right hand side. Lazy reduction is achieved by the pattern which the function call matches against. Function reductions are actually “driven” by patterns in this sense. It is shown that this evaluation mechanism works well for both functional programs and logic programs that involve “executable” functions. As a result, logic programs can be enhanced with (1) the availability of a functional computing environment where there is no notion of backtracking, thus alleviating the degree of control difficulties typically encountered in logic programs, and (2) the ability to terminate “infinite computations” without the introduction of complex control issues at the user-level. On the other hand, functional programs can be equipped with the power of logic programming languages, e.g., Prolog.


title: Creating Efficient Systems for Object-Oriented Languages

authors:
Norihisa Suzuki
Minoru Terada

abstract: Increasingly computer science research has been done using workstations with high-resolution bitmap display systems. Smalltalk-80↑ is a very attractive programming language for such computation environments, since it has very sophisticated graphical systems and programming environments. Unfortunately there are still very few computer systems on which Smalltalk-80 can run with satisfactory speed, and furthermore they are quite expensive. In order to make Smalltalk-80 accessible to a large group of people at low cost,. we have developed compiler techniques useful to generate efficient code for standard register machines such as MC68000. We have also extended Smalltalk-80 to include type expressions, which allow compilers to generate efficient code


title: Stop Losing Sleep Over Incomplete Data Type Specifications

abstract: We give an algorithm to test the completeness of definitions holding on the rewrite systems that they generate. At the opposite of existing techniques that are very restrictive (left-hand sides of definitions must be linear) or rather inefficient our solution is both powerful and efficient. Also, the algorithm that we give detects ambigous or/and incomplete definitions and can tell you why they are ambigous or/and incomplete. It applies too to definitions in presence of equations.


title: A Types-as-Sets Semantics for Milner-Style Polymorphism

abstract: In this paper we present a semantics for Milner-style polymorphism in which types are sets. The basic picture is that our programs are actually terms in a typed λ-calculus, in which the type information can be safely deleted from the concrete syntax. In order to allow for common programming constructs, we allow reflexive or infinite types, and we also allow opaque types, which have private representations.


title: A Hierarchical Basis for Reordering Transformations

abstract: In this paper, we propose a new dependence baaed program representation.This representation is the union of two previously separate concepts: loop carried dependence and hierarchical abstraction.The resulting form has the property that all information necessary to reorder the set of all executions of the statements contained in a given loop exists in the representation of that loop.Thus, this representation provides an ideal basis for reordering transformations such as vectorisation and loop fusion.As evidence of this, we give efficient algorithms for these two transformations based on this representation.


title: Expressional Loops

abstract: This paper proposes an expressional loop notation (XLoop) based on the ideas described in [16,17] which makes it practical to express loops as compositions of functions. The primary benefit of XLoop is that it brings the powerful metaphor of expressions and decomposability to bear on the domain of loops. Wherever this metaphor can be applied, it makes algorithms much easier to construct, understand, and modify.


title: Inverse Currying Transformation on Attribute Grammars

abstract: Inverse currying transformation of an attribute grammar moves a context condition to places in the grammar where the violation of the condition can be detected as soon as the semantic information used in the condition is computed. It thereby takes into account the evaluation order chosen for the attribute grammar. Inverse currying transformations can be used to enhance context sensitive parsing using predicates on attributes, to eliminate sources of backtrack when parsing according to ambiguous grammars, and to facilitate semantics-supported error correction.


title: Efficient Tree Pattern Matching: An Aid to Code Generation

authors:
Alfred V. Aho
Mahadevan Ganapathi

abstract: We show that tree pattern matching has significant advantages in the specification and implementation of efficient code generators. We present a top-down tree-matching algorithm that is particularly well suited to code generation applications. Finally, we present a new back-end language that incorporates tree pattern matching with dynamic programming into a uniform framework for the specification and implementation of efficient code generators.


title: Compiling Path Expressions into VLSI Circuits

authors:
Thomas S. Anantharaman
Edmund M. Clarke
Michael J. Foster
Bud Mishra

abstract: Path expressions were originally proposed by Campbell and Habermann [1] as a mechanism for process synchronization at the monitor level in software. Not unexpectedly, they also provide a useful notation for specifying the behavior of asynchronous circuits. Motivated by this potential application we investigate how to directly translate path expressions into hardware.


title: Semantics-Directed Code Generation

abstract: computer's memory after executionCode generation proceeds by successive reductions.Each transformation corresponds to a machine-operation; the reducer emits one line of assembly code as it performs each reduction:


title: Optimal Scheduling of Arithmetic Operations in Parallel with Memory Accesses

authors:
David Bernstein
Ron Y. Pinter
Michael Rodeh

abstract: We propose a new machine model in which load operations can be performed in parallel with arithmetic operations by two separate functional units. For this model, the evaluation of expression trees is considered. An efficient algorithm to produce an optimal order of evaluation is described and analyzed. For a tree with n vertices the algorithm runs in time Ο(n log2n). If the arithmetic operations have at most two arguments, the complexity goes down to Ο(n logn).


title: Types as Intervals

abstract: To accommodate polymorphic data types and operations, several computer scientists--most notably MacQueen, Plotkin, and Sethi--have proposed formalizing types as ideals. Although this approach is intuitively appealing, the resulting type system is both complex and restrictive because the type constructor that creates function types is not monotonic, and hence not computable. As a result, types cannot be treated as data values, precluding the formalization of type constructors and polymorphic program modules (where types are values) as higher order computable functions. Moreover, recursive definitions of new types do not necessarily have solutions.


title: Analyzing Aliases of Reference Formal Parameters

abstract: Compilers for languages with call-by-reference formal parameters must deal with aliases arising from the renaming effects at call sites. This paper presents a set of techniques for analyzing aliasing patterns. The analysis is divided into detecting the introduction of aliases and tracking their propagation. The algorithm for introduction analysis is simple enough to be performed in a structured editor or parser. A data flow analysis framework is given for the propagation problem, making it possible to solve using standard algorithms from global data flow analysis. Several optimizations are shown which can shrink the size of the problem, and extensions are given to handle ALGOL-style name scoping. Finally, this technique is compared to an alternative implementation strategy and an approximate technique.


title: Modalities for Model Checking: Branching Time Strikes Back

authors:
E. Allen Emerson
Chin-Laung Lei

abstract: Article Modalities for model checking (extended abstract): branching time strikes back Share on Authors: E. Allen Emerson Department of Computer Sciences, University of Texas at Austin, Austin, Texas Department of Computer Sciences, University of Texas at Austin, Austin, TexasView Profile , Chin-Laung Lei Department of Computer Sciences, University of Texas at Austin, Austin, Texas Department of Computer Sciences, University of Texas at Austin, Austin, TexasView Profile Authors Info & Claims POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1985 Pages 84–96https://doi.org/10.1145/318593.318620Online:01 January 1985Publication History 110citation612DownloadsMetricsTotal Citations110Total Downloads612Last 12 Months13Last 6 weeks0 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: On Linearizing Parallel Code

authors:
Jeanne Ferrante
Mary E. Mace

abstract: We consider the problem of generating sequential code for programs written in a language which contains a Multiple GOTO operator, predicates and statements. This problem arises when compiling a parallel intermediate form (such as the PDG [3,4]) to run on a sequential machine; in a source-to-source FORTRAN translator when vectorization of a loop has failed; and when compiling logic designs written in a parallel design language for simulation on a sequential machine. It is easy to generate sequential code for this sort of parallel program if one allows either duplication of code or the insertion of guard variables at merge points; in fact, it is in general impossible without this addition. However, for a large class of parallel programs (such as those originally arising from sequential programs, even after some optimizations have been applied) it is possible to generate sequential code without duplication or the addition of guard variables. In this paper we present an efficient algorithm which will generate sequential code from a parallel program without duplication or additional guard variables for a large class of parallel programs.


title: A Greedy Approach to Incremental Code Generation

authors:
Ray Ford
Duangkaew Sawamiphakdi

abstract: The PSEP System represents a novel approach to incremental compilation for block structured languages. PSEP implements a very fine grain, “greedy” approach as a highly concurrent system of two processes: an editor and a code generator. The design allows the two processes to execute without locking their shared data objects, utilizing semantic information about the concurrent system to guarantee the consistency of the shared objects. This design is compared with the more common “demand” approach to incremental compilation.


title: High-Level Language Facilities for Low-Level Services

authors:
Christopher W. Fraser
David R. Hanson

abstract: EZ is a language-based programming environment that offers the services provided separately by programming languages and operating systems in traditional environments. These services are provided as facilities of a high-level string processing language with a 'persistent' memory in which values exist indefinitely or until changed. In EZ, strings and associative tables provide traditional file and directory services. This paper concentrates on the use of EZ procedures and their activations, which, like other values, have indefinite lifetimes. In EZ, the low-level aspects of procedure execution, such as activation record creation, references to local variables, and access to state information, are accessible via high-level language constructs. As a result, traditionally distinct services can be provided by a single service in the EZ environment. Furthermore, such services can be written in EZ itself. An editor/debugger that illustrates the details of this approach is described.


title: Constraining Control

authors:
Daniel P. Friedman
Christopher T. Haynes

abstract: Continuations, when available as first-class objects, provide a general control abstraction in programming languages. They liberate the programmer from specific control structures, increasing programming language extensibility. Such continuations may be extended by embedding them in functional objects. This technique is first used to restore a fluid environment when a continuation object is invoked. We then consider techniques for constraining the power of continuations in the interest of security and efficiency. Domain mechanisms, which create dynamic barriers for enclosing control, are implemented using fluids. Domains are then used to implement an unwind-protect facility in the presence of first-class continuations. Finally, we demonstrate two mechanisms, wind-unwind and dynamic-wind, that generalize unwind-protect.


title: Principles of OBJ2

authors:
Kokichi Futatsugi
Joseph A. Goguen
Jean-Pierre Jouannaud
José Meseguer

abstract: Article Principles of OBJ2 Share on Authors: Kokichi Futatsugi Electrotechnical Laboratory, 1-1-4 Umezono, Sakura, Niibari, Ibaraki 305, Japan Electrotechnical Laboratory, 1-1-4 Umezono, Sakura, Niibari, Ibaraki 305, JapanView Profile , Joseph A. Goguen SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford University SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford UniversityView Profile , Jean-Pierre Jouannaud CRIN, Campus Scientifique, BP 239, 54506 Vandoeuvre-les-Nancy, Cedex, France CRIN, Campus Scientifique, BP 239, 54506 Vandoeuvre-les-Nancy, Cedex, FranceView Profile , José Meseguer SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford Universit SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford UniversitView Profile Authors Info & Claims POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1985 Pages 52–66https://doi.org/10.1145/318593.318610Online:01 January 1985Publication History 308citation447DownloadsMetricsTotal Citations308Total Downloads447Last 12 Months14Last 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 SiteGet Access


title: Denotational Semantics and Rewrite Rules for FP

authors:
Joseph Y. Halpern
John H. Williams
Edward L. Wimmers
Timothy C. Winkler

abstract: We consider languages whose operational semantics is given by a set of rewrite rules. For such languages, it is important to be able to determine that there are enough rules to completely reduce all meaningful expressions, but not so many that the system of rules is inconsistent. We develop a formal framework in which to give a precise treatment of these soundness and completeness issues. We believe our approach to be novel in that we make heavy use of denotational semantics in our proof of completeness. The particular language for which we answer these questions is an extended version of the functional programming language FP; however the applicability of these techniques extends beyond the realm of FP rewriting systems.


title: The Aggregate Update Problem in Functional Programming Systems

authors:
Paul Hudak
Adrienne G. Bloss

abstract: We discuss the problem of efficiently implementing aggregates (contiguous data structures) such as arrays in functional programming systems. Simple changes to an aggregate conceptually involve making a new copy of the aggregate differing only in the changed component, but such copying can be expensive. We present both static and dynamic techniques for avoiding this copying, and argue that they allow one to program functionally using aggregates, without loss of efficiency over conventional programs.1


title: A Meta-Language and System for Nonlocal Incremental Attribute Evaluation in Language-Based Editors

authors:
Gregory F. Johnson
Charles N. Fischer

abstract: Article Free Access Share on A meta-language and system for nonlocal incremental attribute evaluation in language-based editors Authors: Gregory F. Johnson Cornell University Cornell UniversityView Profile , C. N. Fischer U. of Wisconsin - Madison U. of Wisconsin - MadisonView Profile Authors Info & Claims POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1985Pages 141–151https://doi.org/10.1145/318593.318627Published:01 January 1985Publication History 42citation149DownloadsMetricsTotal Citations42Total Downloads149Last 12 Months14Last 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 Publisher SiteeReaderPDF


title: Matchmaker: An Interface Specification Language for Distributed Processing

authors:
Michael B. Jones
Richard F. Rashid
Mary R. Thompson

abstract: Matchmaker, a language used to specify and automate the generation of interprocess communication interfaces, is presented. The process of and reasons for the evolution of Matchmaker are described. Performance and usage statistics are presented. Comparisons are made between Matchmaker and other related systems. Possible future directions are examined.


title: What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority

abstract: The formal correspondence between an implementation and its specification is examined. It is shown that existing specifications that claim to describe priority are either vacuous or else too restrictive to be implemented in some reasonable situations. This is illustrated with a precisely formulated problem of specifying a first-come-first-served mutual exclusion algorithm, which it is claimed cannot be solved by existing methods.


title: Constraints: A Uniform Approach to Aliasing and Typing

authors:
Leslie Lamport
Fred B. Schneider

abstract: A constraint is a relation among program variables that is maintained throughout execution. Type declarations and a very general form of aliasing can be expressed as constraints. A proof system based upon the interpretation of Hoare triples as temporal logic formulas is given for reasoning about programs with constraints. The proof system is shown to be sound and relatively complete, and example program proofs are given.


title: Logical and Mathematical Reasoning about Imperative Programs

abstract: Logical and mathemlicnl reasoning ahout impcrdtive programs.'


title: Checking That Finite State Concurrent Programs Satisfy Their Linear Specification

authors:
Orna Lichtenstein
Amir Pnueli

abstract: We present an algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program. The running time of the algorithm is exponential in the size of the formula but linear in the size of the checked program. The algorithm yields also a formal proof in case the formula is valid over the program. The algorithm has four versions that check satisfiability by unrestricted, impartial, just and fair computations of the given program.


title: Functional Programming and the Logical Variable

abstract: Logic programming offers a variety of computational effects which go beyond those customarily found in functional programming languages. Among these effects is the notion of the “logical variable.” i.e. a value determined by the intersection of constraints, rather than by direct binding. We argue that this concept is “separable” from logic programming, and can sensibly be incorporated into existing functional languages. Moreover, this extension appears to significantly widen the range of problems which can efficiently be addressed in function form, albeit at some loss of conceptual purity. In particular, a form of side-effects arises under this extension, since a function invocation can exert constraints on variables shared with other function invocations. Nevertheless, we demonstrate that determinacy can be retained, even under parallel execution. The graph reduction language FGL is used for this demonstration, by being extended to a language FGL+LV permitting formal parameter expressions, with variables occurring therein bound by unification. The determinacy argument is based on a novel dataflow-like rendering of unification. In addition the complete partial order employed in this proof is unusual in its explicit representation of demand, a necessity given the “benign” side-effects that arise. An implementation technique is suggested, suitable for reduction architectures.


title: Declaration-Free Type Checking

authors:
Prateek Mishra
Uday S. Reddy

abstract: Conventional Milner-style polymorphic type checkers automatically infer types of functions and simple composite objects such as tuples. Types of recursive data structures (e.g. lists) have to be defined by the programmer through an abstract data type definition. In this paper, we show how abstract data types, involving type union and recursion, can be automatically inferred by a type checker. The language for describing such types is that of regular trees, a generalization of regular expressions to denote sets of tree structured terms. Inference of these types is reducible to the problem of solving simultaneous inclusion inequations over regular trees. We present algorithms to solve such inequations. Using these techniques, programs without any type definitions and type annotations for functions can be type checked.


title: Abstract Types Have Existential Type

authors:
John C. Mitchell
Gordon D. Plotkin

abstract: Article Free Access Share on Abstract types have existential types Authors: John C. Mitchell AT&T Bell Laboratories, Murray Hill, New Jersey AT&T Bell Laboratories, Murray Hill, New JerseyView Profile , Gordon D. Plotkin Department of Computer Science, University of Edinburgh, Edinburgh EH9 3J2 Department of Computer Science, University of Edinburgh, Edinburgh EH9 3J2View Profile Authors Info & Claims POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1985 Pages 37–51https://doi.org/10.1145/318593.318606Published:01 January 1985Publication History 75citation402DownloadsMetricsTotal Citations75Total Downloads402Last 12 Months31Last 6 weeks3 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: A Model and Temporal Proof System for Networks of Processes

authors:
Van Nguyen
David Gries
Susan S. Owicki

abstract: A model and a sound and complete proof system for networks of processes in which component processes communicate exclusively through messages is given. The model, an extension of the trace model, can describe both synchronous and asynchronous networks. The proof system uses temporal-logic assertions on sequences of observations — a generalization of traces. The use of observations (traces) makes the proof system simple, compositional and modular, since internal details can be hidden. The expressive power of temporal logic makes it possible to prove temporal properties (safety, liveness, precedence, etc.) in the system. The proof system is language-independent and works for both synchronous and asynchronous networks.


title: Closurize and Concentrate

authors:
Julian A. Padget
John P. Fitch

abstract: This paper considers current solutions to the problem of representing multiple environments, and uses the results to develop a new model. The motivation is partly a consequence of the renewed interest in the more sophisticated forms of access and control [Sussman & Steele 1978], [Smith 1983]. [Friedman et al. 1984], and partly because the problem identified by Moses [1970] has not, as yet, been satisfactorily resolved. The new model is derived from a consideration of the semantics of identifier binding interrogation. The implementation itself rests on the existence of an environment labeling function which solves a variant of a well known graph theory problem called nearest common ancestor. We describe a suitable implementation of such a function. The new scheme has been implemented in two different LISP systems (Cambridge LISP and Portable Standard LISP), and a third (LISP/VM) is under consideration. In addition, pure deep binding and full shallow binding have both been implemented on top the same base system (Cambridge LISP). Thus it is possible to collect comparisons of the relative efficiencies running simple (stack behavior) programs and complex (multiple context) programs. Some timing results for various tests are given in the final section.


title: Incremental Compilation of Locally Optimized Code

authors:
Lori L. Pollock
Mary Lou Soffa

abstract: Although optimizing compilers have successfully been used to reduce the size and running times of compiled programs, present incremental compilers only support the incremental update of unoptimized code. In this work, we extend the notion of incremental compilation to include optimized code. Techniques to incrementally compile locally optimized code, given intermediate code modifications are developed using a program representation based on flow graphs and dags. A model is designed to represent both unoptimized and optimized code and to maintain an optimizing history. Changes to the optimized code which either destroy optimizations or create conditions for further optimizations are incorporated into the model and the optimized code without recompiling unaffected optimizations.


title: Program Specification and Development in Standard ML

authors:
Donald Sannella
Andrzej Tarlecki

abstract: An attempt is made to apply ideas about algebraic specification in the context of a programming language. Standard ML with modules is extended by allowing axioms in module interface specifications and in place of code. The resulting specification language, called Extended ML, is given a semantics based on the primitive specification-building operations of the kernel algebraic specification language ASL. Extended ML provides a framework for the formal development of programs from specifications by stepwise refinement, which is illustrated by means of a simple example. From its semantic basis Extended ML inherits complete independence from the logical system (institution) used to write specifications. This allows different styles of specification as well as different programming languages to be accommodated.


title: Smart Recompilation

authors:
Walter F. Tichy
Mark C. Baker

abstract: With current compiler technology, changing a single line in a large software system may trigger massive recompilations. If the change occurs in a file with shared definitions, all compilation units depending upon that file must be recompiled to assure consistency. However, many of those recompilations may be redundant, because the change may actually affect only a small fraction of the overall system.


title: Embedding Type Structure in Semantics

abstract: We show how a programming language designer may embed the type structure of a programming language in the more robust type structure of the typed lambda calculus. This is done by translating programs of the language into terms of the typed lambda calculus. Our translation, however, does not always yield a well-typed lambda term. Programs whose translations are not well-typed are considered meaningless, that is, ill-typed. We give a conditionally type-correct semantics for a simple language with continuation semantics. We provide a set of static type-checking rules for our source language, and prove that they are sound and complete: that is, a program passes the typing rules if and only if its translation is well-typed. This proves the correctness of our static semantics relative to the well-established typing rules of the typed lambda-calculus.


title: Constant Propagation with Conditional Branches

authors:
Mark N. Wegman
F. Kenneth Zadeck

abstract: Constant propagation is a well-known global flow analysis problem. The goal of constant propagation is to discover values that are constant on all possible executions of a program and to propagate these constant values as far forward through the program as possible. Expressions whose operands are all constants can be evaluated at compile time and the results propagated further. Using the algorithms presented in this paper can produce smaller and faster compiled programs. The same algorithms can be used for other kinds of analyses (e.g., type determina-tion). We present four algorithms in this paper, all conservative in the sense that all constants may not be found, but each constant found is constant over all possible executions of the program. These algorithms are among the simplest, fastest, and most powerful global constant propagation algorithms known. We also present a new algorithm that performs a form of interprocedural data flow analysis in which aliasing information is gathered in conjunction with constant propagation. Several variants of this algorithm are considered.


title: Logic and Inheritance

authors:
Hassan Aït-Kaci
Roger Nasr

abstract: An elaboration of the Prolog language is described in which the notion of first-order term is replaced by a more general one. This extended form of terms allows the integration of inheritance---an IS-A taxonomy---directly into the unification process rather than indirectly through the resolution-based inference mechanism of Prolog. This results in more efficient computations and enhanced language expressiveness. The language thus obtained, called LOGIN, subsumes Prolog, in the sense that conventional Prolog programs are equally well executed by LOGIN.


title: Operational Semantics of a Parallel Object-Oriented Language

authors:
Pierre America
Jaco de Bakker
Joost N. Kok
Jan J. M. M. Rutten

abstract: The Centre for Mathematics and Computer


title: A Really Abstract Concurrent Model and its Temporal Logic

authors:
Howard Barringer
Ruurd Kuiper
Amir Pnueli

abstract: In this paper we advance the radical notion that a computational model based on the reals provides a more abstract description of concurrent and reactive systems, than the conventional integers based behavioral model of execution sequences. The real model is studied in the setting of temporal logic, and we illustrate its advantages by providing a fully abstract temporal semantics for a simple concurrent language, and an example of verification of a concurrent program within the real temporal logic defined here. It is shown that, by imposing the crucial condition of finite variability, we achieve a balanced formalism that is insensitive to finite stuttering, but can recognize infinite stuttering, a distinction which is essential for obtaining a fully abstract semantics of non-terminating processes. Among other advantages, going into real-based semantics obviates the need for the controversial representation of concurrency by interleaving, and most of the associated fairness constraints.


title: Distributed Data Structures in Linda

authors:
Nicholas Carriero
David Gelernter
Jerrold Leichter

abstract: A distributed data structure is a data structure that can be manipulated by many parallel processes simultaneously. Distributed data structures are the natural complement to parallel program structures, where a parallel program (for our purposes) is one that is made up of many simultaneously active, communicating processes. Distributed data structures are impossible in most parallel programming languages, but they are supported in the parallel language Linda and they are central to Linda programming style. We outline Linda, then discuss some distributed data structures that have arisen in Linda programming experiments to date. Our intent is neither to discuss the design of the Linda system nor the performance of Linda programs, though we do comment on both topics; we are concerned instead with a few of the simpler and more basic techniques made possible by a language model that, we argue, is subtly but fundamentally different in its implications from most others.This material is based upon work supported by the National Science Foundation under Grant No. MCS-8303905. Jerry Leichter is supported by a Digital Equipment Corporation Graduate Engineering Education Program fellowship.


title: A Parallel Language and its Compilation to Multiprocessor Machines or VLSI

abstract: A language Crystal and its compiler for parallel programming is presented. The goal of Crystal is to help programmers in seeking efficient parallel implementations of an algorithm, and managing the complexity that might arise in dealing with hundreds of thousands of autonomous parallel processes. In Crystal, a program consists of a system of recursion equations and is interpreted as a parallel system. Crystal views a large complex system as consisting of a hierarchy of parallel sub-systems, built upon a set of Crystal programs by composition and abstraction. There is no mention of explicit communications in a Crystal program. The Crystal compiler automatically incorporates pipelining into programs, and generates a parallel program that is optimal with respect to an algorithm. Each optimizing compiler, targeted for a particular machine, determines the appropriate granular size of parallelism and attains a balance between computations and communications. Based on the language, a unified theory for understanding and generating any systolic design has been devised and it constitues a part of the compiler.


title: Retargetable High-Level Alias Analysis

abstract: All optimizing compilers must deal with the problem of aliases arising due to the presence of multiple names that reference the same memory areas. Presented in this paper is a staged, high-level alias analysis methodology that provides detailed alias information to a global optimizer implemented at any level in the compilation process. The framework provides easy portability of optimizing compilers to new architectures, as well as the easy addition, of new compilers to an already existing family of optimizing compilers. The method involves the application of a set of language-specific alias rules to the source code in order to gather alias information. A language-independent component then performs a transitive closure of this information and transforms it into a presentation more suitable for use by a global optimizer. Each stage of the methodology is detailed. Results are given for an implemented family of compilers targeted for a reduced instruction set computer.


title: Code Motion of Control Structures in High-Level Languages

authors:
Ron Cytron
Andy Lowry
F. Kenneth Zadeck

abstract: One trend among programmers is the increased use of abstractions. Through encapsulation techniques, abstractions extend the repertory of data structures and their concomitant operations that are processed directly by a compiler. For example, a compiler might not offer sets or set operations in its base language, but abstractions allow a programmer to define sets in terms of constructs already recognized by the compiler. In particular, abstractions can allow new constructs to be defined in terms of other abstractions. Although significant power is gained through the use of layered abstractions, object code quality suffers as increasingly less of a program's data structures and operations are exposed to the optimization phase of a compiler. Multiple references to abstractions are also inefficient, since the interaction between abstractions is often complex yet hidden from a compiler. Abstractions are most flexible when they are cast in general terms; a specific invocation is then tailored by the abstraction to obtain the appropriate code. A sequence of references to such abstractions can be inefficient due to functional redundancy that cannot be detected at compile-time. By integrating the references, the offending segments of code can be moved to a more advantageous position. Although procedure integration materializes abstracted constructs, the abstractions can still be ineligible for optimization using current techniques; in particular, abstractions often involve loops and conditional branches that can obscure code that would otherwise be eligible for code motion.


title: Atomic Data Abstractions in a Distributed Collaborative Editing System

authors:
Irene Greif
Robert Seliger
William E. Weihl

abstract: This paper describes our experience implementing CES, a distributed Collaborative Editing System written in Argus, a language that includes facilities for managing long-lived distributed data. Argus provides atomic actions, which simplify the handling of concurrency and failures, and mechanisms for implementing atomic data types, which ensure serializability and recoverability of actions that use them. This paper focuses on the support for atomicity in Argus, especially the support for building new atomic types. Overall the mechanisms in Argus made it relatively easy to build CES; however, we encountered interesting problems in several areas. For example, much of the processing of an atomic action in Argus is handled automatically by the run-time system; several examples are presented that illustrate areas where more explicit control in the implementations of atomic types would be useful.


title: High-Quality Code Generation Via Bottom-Up Tree Pattern Matching

authors:
Philip J. Hatcher
Thomas W. Christopher

abstract: High-quality local code generation is one of the most difficult tasks the compiler-writer faces. Even if register allocation decisions are postponed and common subexpressions are ignored, instruction selection on machines with complex addressing can be quite difficult. Efficient and general algorithms have been developed to do instruction selection, but these algorithms fail to always find optimal solutions. Instruction selection algorithms based on dynamic programming or complete enumeration always find optimal solutions, but seem to be too costly to be practical. This paper describes a new instruction selection algorithm, and its prototype implementation, based on bottom-up tree pattern-matching. This algorithm is both time and space efficient, and is capable of doing optimal instruction selection for the DEC VAX-11 with its rich set of addressing modes.


title: Dynamically Bypassing Copy Rule Chains in Attribute Grammars

abstract: Attribute grammars require copy rules to transfer values between attribute instances distant in an attributed parse tree. We introduce copy bypass attribute propagation that dynamically replaces copy rules with nonlocal dependencies, resulting in faster incremental evaluation. A evaluation strategy is used that approximates a topological ordering of attribute instances. The result is an efficient incremental evaluator that allows multiple subtree replacement on any noncircular attribute grammar.


title: Para-Functional Programming: A Paradigm for Programming Multiprocessor Systems

authors:
Paul Hudak
Lauren Smith

abstract: One of the most important pragmatic advantages of functional languages is that concurrency in a program is implicit -- there is no need for special constructs to express parallelism as is required in most conventional languages. Furthermore, it is fairly easy for compilers to automatically determine the concurrency as a step toward decomposing a program for execution on a suitable parallel architecture. Yet it is often the case that one knows precisely the optimal decomposition for execution on a particular machine, and one can never expect a compiler to determine such optimal mappings in all cases. This paper is concerned with ways to allow the programmer to explicitly express this mapping of program to machine, by using annotations that, given a few minor constraints, cannot alter the functional semantics of the program. We show through several detailed examples the expressiveness and conciseness of the resulting para-functional programming methodology, using an experimental language called ParAlfl based on our ideas. We also give a formal denotational description of the mapping semantics using a notion of execution trees.This research was supported in part by NSF Grants DCR-8403304 and DCR-8451415, and a Faculty Development Award from IBM.


title: Higher-Order Strictness Analysis in Untyped Lambda Calculus

authors:
Paul Hudak
Jonathan Young

abstract: A function is said to be strict in one of its formal parameters if, in all calls to the function, either the corresponding actual parameter is evaluated, or the call does not terminate. Detecting which arguments a function will surely evaluate is a problem that arises often in program transformation and compiler optimization. We present a strategy that allows one to infer strictness properties of functions expressed in the lambda calculus. Our analysis improves on previous work in that (1) a set-theoretic characterization of strictness is used that permits treatment of free variables, which in turn permits a broader range of interpretations, and (2) the analysis provides an effective treatment of higher-order functions. We also prove a result due to Meyer [15]: the problem of first-order strictness analysis is complete in deterministic exponential time. However, because the size of most functions is small, the complexity seems to be tractable in practice.This research was supported in part by NSF Grant MCS-8302018, and a Faculty Development Award from IBM.


title: Executable Specifications with Quantifiers in the FASE System

authors:
Stan Jefferson
Samuel N. Kamin

abstract: We present an overview of the FASE system for executable specifications based upon final, rather than initial, algebras. Particular emphasis is placed upon the execution of expressions involving quantifiers. The need for such expressions is explained, as is our method for evaluating them. By permitting quantifiers, we are able to give very natural specifications for many data types. As an example, we give the FASE specification of Kemmerer's library system.


title: A Maximum-Flow Approach to Anomaly Isolation in Unification-Based Incremental Type Inference

authors:
Gregory F. Johnson
Janet A. Walz

abstract: A crucial aspect of a program intended for general use is its behavior in the presence of erroneous inputs. For instance, much attention has been devoted to the problems of error detection, reporting, and correction in compilers1,2. As programming languages and systems based in one way or another on unification3 become more common, it becomes increasingly important to develop a theory of error detection and correction for unification-based systems. We report here on a language-based editor for a variant of ML4 that uses a novel approach to the isolation of likely causes of user errors. As the user edits and manipulates his or her program, unification is incrementally applied to determine its type correctness. If a type inconsistency arises, a maximum flow technique is applied to the set of type equations to determine the most likely source of error. In this way a determination can be made as to the relative strengths with which the set of type equations asserts multiple contradictory hypotheses. In a language such as ML, the type of an object is inferred from patterns of usage. Often it is the case that most uses of a given object are mutually consistent, whereas one or a very small number of uses conflict with the general usage pattern. In MOE (ML-Oriented Editor), if it is possible to discern that such a situation has arisen, likely errors are highlighted at high intensity and all other program components that contributed to the inferred type of the object are highlighted at a lower intensity. In providing error information to the user, two principles are observed:(1) Error indications should be complete but parsimonious; the user should see highlighted on the screen everything that contributed directly to an error, but nothing. more,(2) The user's attention should be drawn to what appear to be the anomalies that are responsible for errors.Language-based editors permit a new level of quality in the process of helping users when inputs are, for one reason or another, invalid. Unification-based type inference in language-based editors appears to have been first considered by Meertens 5. Snelting and Bahlke have more recently also explored this approach.


title: Data Flow Analysis of Applicative Programs Using Minimal Function Graphs

authors:
Neil D. Jones
Alan Mycroft

abstract: Data or program flow analysis is concerned with the static analysis of programs, to obtain as much information as possible about their possible run time behavior without actually having to run the programs. Due to the unsolvability of the halting problem (and nearly any other question concerning program behavior), such analyses are necessarily only approximate whenever the analysis algorithm is guaranteed to terminate. Further, exact analysis may be impossible due to the lack of knowledge of input data values, so the analysis can at best yield information about sets of possible computations.


title: Hierarchical VLSI Design Systems Based on Attribute Grammars

authors:
Larry G. Jones
Janos Simon

abstract: The attribute grammar technique used for design of structure editors is suggested as a foundation for building hierarchical incremental design editors for VLSI circuits. The usual definition of attribute grammars is extended: the cycles that occur in VLSI design make us come to terms with circular attributes (under conditions that guarantee their least fixpoint solution, namely that the functions be monotone and yield values over a lattice of bounded height). Many interesting VLSI design problems can be cast in attributes meeting this condition, for example, timing verification, logic simulation, power dissipation, and adherence to clocking disciplines, to name a few. As an illustration of the formalism, attributes are presented which solve the All Bidirectional Edges problem that labels the direction of information flow in a circuit. The incremental evaluation algorithm of [Rep82] is extended to handle fixpoint computations of circular attributes by noting that when the dependency graph is broken into its strongly connected components, a directed acyclic graph results. The worst-case running time of the resulting incremental evaluation algorithm is bounded by O (hk |AFFECTEDSCC|), where h is the height of the largest attribute lattice, k the largest number of attributes in any one strongly connected component, and |AFFECTEDSCC| the number of strongly connected components affected by a single modification to the design tree.


title: Compilers and Staging Transformations

authors:
Ulrik Jørring
William L. Scherlis

abstract: Computations can generally be separated into stages, which are distinguished from one another by either frequency of execution or availability of data. Precomputation and frequency reduction involve moving computation among a collection of stages so that work is done as early as possible (so less time is required in later steps) and as infrequently as possible (to reduce overall time).We present, by means of examples, several general transformation techniques for carrying out precomputation transformations. We illustrate the techniques by deriving fragments of simple compilers from interpreters, including an example of Prolog compilation, but the techniques are applicable in a broad range of circumstances. Our aim is to demonstrate how perspicuous accounts of precomputation and frequency reduction can be given for a wide range of applications using a small number of relatively straightforward techniques.Related work in partial evaluation, semantically directed compilation, and compiler optimization is discussed.


title: Global Storage Allocation in Attribute Evaluation

authors:
Takuya Katayama
Hisashi Sasaki

abstract: Global storage allocation for attributes in an attribute grammar evaluator is discussed and an algorithm for determining if a given set of attribute occurrences can share a common global storage is obtained.


title: Towards Programming with Knowledge Expressions

abstract: Explicit use of knowledge expressions in the design of distributed algorithms is explored. A non-trivial case study is carried through, illustrating the facilities that a design language could have for setting and deleting the knowledge that the processes possess about the global state and about the knowledge of other processes. No implicit capabilities for logical reasoning are assumed. A language basis is used that allows common knowledge not only by an eager protocol but also in the true sense. The observation is made that the distinction between these two kinds of common knowledge can be associated with the level of abstraction: true common knowledge of higher levels of abstraction: true common knowledge of higher levels can be implemented as eager common knowledge on lower levels. A knowledge-motivated abstraction tool is therefore suggested to be useful in supporting stepwise refinement of distributed algorithms.


title: A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks

authors:
Christian Lengauer
Chua-Huang Huang

abstract: Our concern is the mechanical certification of transformations of sequential program executions into parallel executions with equivalent semantics. The objective of such transformations is to accelerate the execution of programs. The result reported here is a mechanically certified theorem of optimality. We present a transformation which applies to every program in a particular programming language, the language of sorting networks. This transformation transforms the sequential execution of any sorting network into an execution which is as fast or faster than any other transformation which applies to every sorting network. The theorem is stated formally in a mechanized logic.


title: Limitations of Synchronous Communication with Static Process Structure in Languages for Distributed Computing

authors:
Barbara Liskov
Maurice Herlihy
Lucy Gilbert

abstract: Modules in a distributed program are active, communicating entities. A language for distributed programs must choose a set of communication primitives and a structure for processes. This paper examines one possible choice: synchronous communication primitives (such as rendez-vous or remote procedure call) in combination with modules that encompass a fixed number of processes (such as Ada tasks or UNIX processes). An analysis of the concurrency requirements of distributed programs suggests that this combination imposes complex and indirect solutions to common problems and thus is poorly suited for applications such as distributed programs in which concurrency is important. To provide adequate expressive power, a language for distributed programs should abandon either synchronous communication primitives or the static process structure.


title: Using Dependent Types to Express Modular Structure

abstract: Writing any large program poses difficult problems of organization. In many modern programming languages these problems are addressed by special linguistic constructs, variously known as modules, packages, or clusters, which provide for partitioning programs into manageable components and for securely combining these components to form complete programs. Some general purpose components are able to take on a life of their own, being separately compiled and stored in libraries of generic, reusable program units. Usually modularity constructs also support some form of information hiding, such as "abstract data types." "Programming in the large" is concerned with using such constructs to impose structure on large programs, in contrast to "programming in the small", which deals with the detailed implementation of algorithms in terms of data structures and control constructs. Our goal here is to examine some of the proposed linguistic notions with respect to how they meet the pragmatic requirements of programming in the large.


title: "Type" Is Not A Type

authors:
Albert R. Meyer
Mark B. Reinhold

abstract: A function has a dependent type when the type of its result depends upon the value of its argument. Dependent types originated in the type theory of intuitionistic mathematics and have reappeared independently in programming languages such as CLU, Pebble, and Russell. Some of these languages make the assumption that there exists a type-of-all-types which is its own type as well as the type of all other types. Girard proved that this approach is inconsistent from the perspective of intuitionistic logic. We apply Girard's techniques to establish that the type-of-all-types assumption creates serious pathologies from a programming perspective: a system using this assumption is inherently not normalizing, term equality is undecidable, and the resulting theory fails to be a conservative extension of the theory of the underlying base types. The failure of conservative extension means that classical reasoning about programs in such a system is not sound.


title: Representation Independence and Data Abstraction

abstract: One purpose of type checking in programming languages is to guarantee a degree of "representation independence:" programs should not depend on the way stacks are represented, only on the behavior of stacks with respect to push and pop operations. In languages with abstract data type declarations, representation independence should hold for user-defined types as well as built-in types. We study the representation independence properties of a typed functional language (second-order lambda calculus) with polymorphic functions and abstract data type declarations in which data type implementations (packages) may be passed as function parameters and returned as results. The type checking rules of the language guarantee that two data type implementations P and Q are equivalence whenever there is a correspondence between the behavior of the operations of P and the behavior of the operations of Q.


title: Annotations for Distributed Programming in Logic

authors:
Raghu Ramakrishnan
Abraham Silberschatz

abstract: It has been recognised that languages like Concurrent Prolog and Parlog which use committed choice non-determinism have departed from the original concept of logic programming, but no new paradigm has been suggested. In this paper we propose that programs in such languages be viewed as rewrite rules that hierarchically decompose a process into a network of distributed processes. Logical variables and unification provide a powerful means of communication, and annotations can provide a synchronization mechanism that complements them.


title: Remote Attribute Updating for Language-Based Editors

authors:
Thomas W. Reps
Carla Marceau
Tim Teitelbaum

abstract: A major drawback to the use of attribute grammars in language-based editors has been that attributes can only depend on neighboring attributes in a program's syntax tree. This paper concerns new attribute-grammar-based methods that, for a suitable class of grammars, overcome this fundamental limitation. The techniques presented allow the updating algorithm to skip over arbitrarily large sections of the tree that more straightforward updating methods visit node by node. These techniques are then extended to deal with aggregate values, so that the attribute updating procedure need only follow dependencies due to a changed component of an aggregate value. Although our methods work only for a restricted class of attribute grammars, satisfying the necessary restrictions should not place an undue burden on the writer of the grammar.


title: Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis

authors:
Gregor Snelting
Wolfgang Henhapl

abstract: Language-specific editors for typed programming languages must contain a subsystem for semantic analysis in order to guarantee correctness of programs with respect to the context conditions of the language. As programs are usually incomplete during development, the semantic analysis must be able to cope with missing context information, e. g. incomplete variable declarations or calls to procedures imported from still missing modules. In this paper we present an algorithm for incremental semantic analysis, which guarantees immediate detection of semantic errors even in arbitrary incomplete program fragments. The algorithm is generated from the language's context conditions, which are described by inference rules. During editing, these rules are evaluated using a unification algorithm for many-sorted algebras with semi-lattice ordered subsorts and non-empty equational theories. The method has been implemented as part of the PSG system, which generates interactive programming environments from formal language definitions, and has been successfully used to generate an incremental semantic analysis for PASCAL and MODULA-2.


title: Finding the Source of Type Errors

abstract: It is a truism that most bugs are detected only at a great distance from their source. Although polymorphic type-checking systems like those in ML help greatly by detecting potential run-time type errors at compile-time, such systems are still not very helpful for locating the source of a type error. Typically, an error is reported only when the type-checker can proceed no further, even though the programmer's actual error may have occurred much earlier in the text. We describe an algorithm which appears to be quite helpful in isolating and explaining the source of type errors. The algorithm works by keeping track of the reasons the checker makes deductions about the types of variables.


title: Expressing Interesting Properties of Programs in Propositional Temporal Logic

abstract: We show that the class of properties of programs expressible in propositional temporal logic can be substantially extended if we assume the programs to be data-independent. Basically, a program is data-independent if its behavior does not depend on the specific data it operates upon. Our results significantly extend the applicability of program verification and synthesis methods based on propositional temporal logic.


title: Equational Logic Programming: An Extension to Equational Programming

authors:
Jia-Huai You
P. A. Subrahmanyam

abstract: The paradigm of equational programming potentially possesses all the features provided by Prolog-like languages. In addition, the ability to reason about equations, which is not provided by Prolog, can be accommodated by equational languages. In this paper, we propose an extended equational programming paradigm, and describe an equational logic programming language which is an extension of the equational language defined in [Hoff82]. Semantic foundations for the extension are discussed. The extended language is a powerful logic programming language in the sense of Prolog and thus enjoys the programming features that Prolog possesses. Furthermore, it provides an ability to solve equations, which captures the essential power of equational programming.


title: Automatic Decomposition of Scientific Programs for Parallel Execution

authors:
Randy Allen
David Callahan
Ken Kennedy

abstract: An algorithm for transforming sequential programs into equivalent parallel programs is presented. The method concentrates on finding loops whose separate iterations can be run in parallel without syn-chronization. Although a simple version of the method can be shown to be optimal, the problem of generating optimal code when loop interchange is employed is shown to be intractable. These methods are implemented in an experimental translation system developed at Rice University. 1.


title: Appraising Fairness in Languages for Distributed Programming

authors:
Krzysztof R. Apt
Nissim Francez
Shmuel Katz

abstract: The relations among various languages and models for distributed computation and various possible definitions of fairness are considered. Natural semantic criteria are presented which an acceptable notion of fairness should satisfy. These are then used to demonstrate differences among the basic models, the added power of the fairness notion, and the sensitivity of the fairness notion to irrelevant semantic interleavings of independent operations. These results are used to show that from the considerable variety of commonly used possibilities, only strong process fairness is appropriate for CSP if these criteria are adopted. We also show that under these criteria, none of the commonly used notions of fairness are fully acceptable for a model with an n-way synchronization mechanism. Finally, the notion of fairness most often mentioned for Ada is shown to be fully acceptable.


title: Scheduling Arithmetic and Load Operations in Parallel with No Spilling

authors:
David Bernstein
Jeffrey M. Jaffe
Michael Rodeh

abstract: We consider a machine model in which load operations can be performed in parallel with arithmetic operations by two separate functional units. For this model, the evaluation of a set of expression trees is discussed. A dynamic programming algorithm to produce an approximate solution is described and analyzed. For binary trees its worse case cost is at most 9.1% worse than the optimal cost.


title: Binding Performance at Language Design Time

authors:
Jiazhen Cai
Robert Paige

abstract: An important research goal in software engineering and programming languages is the development of principles underlying the specification of computable problems, the translation of these problems into efficient and correct programs, and the performance analysis of these programs. This paper uncovers some of these principles, which are used to design a problem specification language L1 restricted to problems that can be compiled automatically into programs whose worst case asymptotic time and space complexities are linear in the input/output space. Any problem expressible in L1 can be compiled into a linear cost program. A compiler for L1 has been implemented in the RAPTS transformational programming system.


title: Lustre: A Declarative Language for Programming Synchronous Systems

authors:
Paul Caspi
Daniel Pilaud
Nicolas Halbwachs
John Plaice

abstract: LUSTRE is a synchronous data-flow language for programming systems which interact with their environments in real-time. After an informal presentation of the language, we describe its semantics by means of structural inference rules. Moreover, we show how to use this semantics in order to generate efficient sequential code, namely, a finite state automaton which represents the control of the program. Formal rules for program transformation are also presented.


title: An Improvement to Bottom-up Tree Pattern Matching

abstract: Article Free Access Share on An improvement to bottom-up tree pattern matching Author: D. R. Chase Department of Computer Science, Rice University, Houston, Texas Department of Computer Science, Rice University, Houston, TexasView Profile Authors Info & Claims POPL '87: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesOctober 1987Pages 168–177https://doi.org/10.1145/41625.41640Published:01 October 1987Publication History 56citation855DownloadsMetricsTotal Citations56Total Downloads855Last 12 Months79Last 6 weeks7 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 Publisher SiteeReaderPDF


title: Extensions for Multi-Module Records in Conventional Programming Languages

authors:
David R. Cheriton
Michael E. Wolf

abstract: An extended record facility is described that supports multi-module records by providing:


title: A Calculus for Assignments in Higher-Order Languages

authors:
Matthias Felleisen
Daniel P. Friedman

abstract: Imperative assignments are abstractions of recurring programming patterns in purely functional programming languages. When added to higher-order functional languages, they provide a higher-level of modularity and security but invalidate the simple substitution semantics. We show that, given an operational interpretation of a denotational semantics for such a language, it is possible to design a two-level extension of the lu-calculus. This calculus provides a location-free rewriting semantics of the language and offers new possibilities for reasoning with assignments. The upper level of the calculus factors out all the steps in a reduction sequence which must be in a linear order; the lower level allows a partial ordering of reduction steps.


title: Environments as First Class Objects

authors:
David Gelernter
Suresh Jagannathan
Thomas London

abstract: We describe a programming language called Symmetric Lisp that treats environments as firstclass objects. Symmetric Lisp allows programmers to write expressions that evaluate to environments, and to create and denote variables and constants of type environment as well. One consequence is that the roles filled in other languages by a variety of limited, special purpose environment forms like records, structures, closures, modules, classes and abstract data types are filled instead by a single versatile and powerful structure. In addition to being its fundamental structuring tool, environments also serve as the basic functional object in the language. Because the elements of an environment are evaluated in parallel, Symmetric Lisp is a parallel programming language; because they may be assembled dyamically as well as statically, Symmetric Lisp accomodates an unusually flexible and simple (parallel) interpreter as well as other historysensitive applications requiring dynamic environments. We show that firstclass environments bring about fundamental changes in a language's structure: conventional distinctions between declarations and expressions, data structures and program structures, passive modules and active processes disappear. We argue that the resulting language is clean, simple and powerful.


title: Compiling Strictness into Streams

authors:
Cordelia V. Hall
David S. Wise

abstract: Article Free Access Share on Compiling strictness into streams Authors: C. V. Hall Indiana University, 101 Lindley Hall, Bloomington, Indiana, U.S.A. Indiana University, 101 Lindley Hall, Bloomington, Indiana, U.S.A.View Profile , D. S. Wise Indiana University, 101 Lindley Hall, Bloomington, Indiana, U.S.A. Indiana University, 101 Lindley Hall, Bloomington, Indiana, U.S.A.View Profile Authors Info & Claims POPL '87: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesOctober 1987 Pages 132–143https://doi.org/10.1145/41625.41637Online:01 October 1987Publication History 15citation176DownloadsMetricsTotal Citations15Total Downloads176Last 12 Months5Last 6 weeks0 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: Axioms for Concurrent Objects

authors:
Maurice Herlihy
Jeannette M. Wing

abstract: Specification and verification techniques for abstract data types that have been successful for sequential programs can be extended in a natural way to provide the same benefits for concurrent programs. We propose an approach to specifying and verifying concurrent objects based on a novel correctness condition, which we call “linearizability.” Linearizability provides the illusion that each operation takes effect instantaneously at some point between its invocation and its response, implying that the meaning of a concurrent object's operations can still be given by pre- and post-conditions. In this paper, we will define and discuss linearizability, and then give examples of how to reason about concurrent objects and verify their implementations based on their (sequential) axiomatic specifications.


title: Full Abstraction of a Real-Time Denotational Semantics for an Occam-like Language

authors:
Cornelis Huizing
Rob Gerth
Willem P. de Roever

abstract: We present a fully abstract semantics for real-time distributed computing of the Ada and OCCAM kind in a denotational style. This semantics turns termination, communication along channels, and the time communication takes place, into observables. Yet it is the coarsest semantics to do so which is syntax-directed (this is known as full abstraction). It extends the linear history semantics for CSP of Francez, Lehman and Pnueli. Our execution model is based on maximizing concurrent activity as opposed to interleaving (in which only one action occurs at the time and arbitrary delays are incurred between actions). It is a variant of the maximal parallelism model of Salwicki and Müldner.


title: Constraint Logic Programming

authors:
Joxan Jaffar
Jean-Louis Lassez

abstract: We address the problem of designing programming systems to reason with and about constraints. Taking a logic programming approach, we define a class of programming languages, the CLP languages, all of which share the same essential semantic properties. From a conceptual point of view, CLP programs are highly declarative and are soundly based within a unified framework of formal semantics. This framework not only subsumes that of logic programming, but satisfies the core properties of logic programs more naturally. From a user's point of view, CLP programs have great expressive power due to the constraints which they naturally manipulate. Intuition in the reasoning about programs is enhanced as a result of working directly in the intended domain of discourse. This contrasts with working in the Herbrand Universe wherein every semantic object has to be explicitly coded into a Herbrand term; this enforces reasoning at a primitive level. Finally, from an implementor's point of view, CLP systems can be efficient because of the exploitation of constraint solving techniques over specific domains.


title: Semantic Parallelization: A Practical Exercise in Abstract Interpretation

abstract: The parallelization of sequential programs is an adequate approach for the easy use of architectural features provided on parallel computers. We propose to enhance this technique with the notion of semantic parallelization. The principle is to consider the transformations of programs induced by parallelization as non-standard denotational semantics of the source programming language. We show how to apply this concept to detect, in a toy language ALL, parallelizable complex commands and to deal with some type of programs using indirections. Thanks to results in domain theory and abstract interpretation, we give correctness proofs for these transformations with respect to ALL standard semantic. A byproduct of our approach is that a denotational specification is also an executable prototype ;hence, we were able to implement a semantic parallelizer in the ML functional language. Running examples are supplied.