POPL

Previous attempts at vectorizing programs written in a sequential high level language focused on converting control dependences to data dependences using a mechanism known as IF-conversion. After IF-conversion vector optimizations are performed on a ...

Program dependence graphs are an important program representation technique for use in vectorization, parallelization and programming environments. We present a graph rewriting semantics for program dependence graphs and prove the equivalence between ...

Circular attribute grammars appear in many data flow analysis problems. As one way of making the notion useful, an automatic translation of circular attribute grammars to equivalent non-circular attribute grammars is presented. It is shown that for ...

We present a new algorithm for computing interprocedural aliases due to passing parameters by reference. This algorithm runs in O(N²+NE) time and, when combined with algorithms for alias-free, flow-insensitive data-flow problems, yields algorithms for ...

This paper presents type classes, a new approach to ad-hoc polymorphism. Type classes permit overloading of arithmetic operators such as multiplication, and generalise the “eqtype variables” of Standard ML. Type classes extend the Hindley/Milner ...

Strongly typed languages with records may have inclusion rules so that records with more fields can be used instead of records with less fields. But these rules lead to a global treatment of record types as a special case. We solve this problem by ...

We define in this paper a notion of realizability for the Calculus of Constructions. The extracted programs are terms of the Calculus that do not contain dependent types. We introduce a distinction between informative and non-informative propositions. ...

We study the complexity of type inference for a core fragment of ML with lambda abstraction, function application, and the polymorphic let declaration. Our primary technical tool is the unification problem for a class of “polymorphic” type expressions. ...

Most of the theoretical work on the semantics of logic programs assumes an interpreter that provides a complete resolution procedure. In contrast, for reasons of efficiency, most logic programming languages are built around incomplete procedures. This ...

CLP^*(D) is a class of constraint logic programming languages which incorporates the notion of abstraction. Predicates in CLP^*(D) are (potentially) infinite rational trees which represent abstractions of constraint expressions. This view of predicates as ...

We propose a framework for discussing fully abstract compositional semantics, which exposes the interrelations between the choices of observables, compositions, and meanings. Every choice of observables and compositions determines a unique fully ...

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

The calculus is an extension of CCS [Mil80] in the sense ...

A dataflow network consists of nodes that communicate over perfect FIFO channels. For dataflow networks containing only deterministic nodes, a simple and elegant semantic model has been presented by Kahn. However, for nondeterministic networks, the ...

There has been much interest in decision procedures for testing satisfiability (or validity) of formulae in various systems of Temporal Logic. This is due to the potential applications of such decision procedures to mechanical reasoning about ...

We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) is valid ...

Methods for synthesizing concurrent programs from Temporal Logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson & Clarke [EC82] and Manna & Wolper [MW84]. An important advantage ...

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

Statically-typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type-consistency checks are performed at runtime. However, ...

A new general notion of model for the polymorphic lambda calculus based on the simple idea of a universe, is proposed. Although impossible in nonconstructive set theory, the notion is unproblematic for constructive sets, yields completeness and ...

The definitions of Conjunctive types and their subtype relation, as introduced by Coppo-Dezani, are extended to consider the conjunction as a partial mapping from pairs of types to types, and the subtype relation as a relation between finite sets of ...

The theory of term rewriting systems has important applications in abstract data type specifications and functional programming languages. We begin here a study of properties of systems that are not necessarily terminating, but allow for infinite ...

We introduce a programming paradigm in which statements are constraints over partial orders. A partial order programming problem has the form minimize u subject to u₁ ⊒ v₁, u₂ ⊒ v₂, ··· where u is the goal, and u₁ ⊒ v₁, u₂ ⊒ v₂, ··· is a collection of ...

This paper addresses semantic and expressiveness issues for temporal logic programming and in particular for the TEMPLOG language proposed by Abadi and Manna. Two equivalent formulations of TEMPLOG's declarative semantics are given: in terms of a ...

Using concepts from denotational semantics, we have produced a very simple compiler that can be used to compile standard programming languages and produces object code as efficient as that of production compilers. The compiler is based entirely on ...

We implemented a continuation-passing style (CPS) code generator for ML. Our CPS language is represented as an ML datatype in which all functions are named and most kinds of ill-formed expressions are impossible. We separate the code generation into ...

Copy elimination is an important optimization for compiling functional languages. Copies arise because these languages lack the concepts of state and variable; hence updating an object involves a copy in a naive implementation. Copies are also possible ...

This paper concerns the algebraic specification of abstract data types. It introduces and motivates the recently-developed framework of unified algebras, and provides a practical notation for their modular specification. It also compares unified ...

We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm with ...