2,199 papers · page 89 of 110
We consider monotone input/output automata, which model a usefully large class of dataflow networks of indeterminate (or nonfunctional) processes. We obtain a characterization of the relations computable by these automata, which states that a relation R : X ! 2 Y (viewed as a "no…
We need a programming model that combines the advantages of the synchronous and asynchronous parallel styles. Synchronous programs are determinate (thus easier to reason about) and avoid synchronization overheads. Asynchronous programs are more flexible and handle conditionals mo…
We present a new approach to dynamic typing in a static framework. Our main innovation is the use of structural subtyping for dynamic types based on the idea that possible dynamic typing as a property should be inherited by objects of all types. Two properties of our system set i…
Statically-typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type-consistency checks are performed at runtime. However, even in statically-type lang…
We implemented a continuation-passing style (CPS) code generator for ML. Our CPS language is represented as an ML datatype in which all functions are named and most kinds of ill-formed expressions are impossible. We separate the code generation into phases that rewrite this repre…
Methods for synthesizing concurrent programs from Temporal Logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson & Clarke [EC82] and Manna & Wolper [MW84]. An important advantage of these synthesis methods …
This paper addresses semantic and expressiveness issues for temporal logic programming and in particular for the TEMPLOG language proposed by Abadi and Manna. Two equivalent formulations of TEMPLOG's declarative semantics are given: in terms of a minimal Herbrand model and in ter…
Previous attempts at vectorizing programs written in a sequential high level language focused on converting control dependences to data dependences using a mechanism known as IF-conversion. After IF-conversion vector optimizations are performed on a data dependence graph. However…
This paper presents an overview of the programming language Modula-3, and a more detailed description of its type system.
We present a new algorithm for computing interprocedural aliases due to passing parameters by reference. This algorithm runs in O(N2+NE) time and, when combined with algorithms for alias-free, flow-insensitive data-flow problems, yields algorithms for solution of the general flow…
Article An efficient method of computing static single assignment form Share on Authors: R. Cytron IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NYView Profile , J. Ferrante IBM Res…
We study properties of rewrite systems that are not necessarily terminating, but allow instead for transfinite derivations that have a limit.In particular, we give conditions for the existence of a limit and for its uniqueness and relate the operational and algebraic semantics of…
There has been much interest in decision procedures for testing satisfiability (or validity) of formulae in various systems of Temporal Logic. This is due to the potential applications of such decision procedures to mechanical reasoning about correctness of concurrent programs. W…
We propose a framework for discussing fully abstract compositional semantics, which exposes the interrelations between the choices of observables, compositions, and meanings. Every choice of observables and compositions determines a unique fully abstract equivalence. A semantics …
Copy elimination is an important optimization for compiling functional languages. Copies arise because these languages lack the concepts of state and variable; hence updating an object involves a copy in a naive implementation. Copies are also possible if proper targeting has not…
CLP*(D) is a class of constraint logic programming languages which incorporates the notion of abstraction. Predicates in CLP*(D) are (potentially) infinite rational trees which represent abstractions of constraint expressions. This view of predicates as constraint abstractions wa…
A dataflow network consists of nodes that communicate over perfect FIFO channels. For dataflow networks containing only deterministic nodes, a simple and elegant semantic model has been presented by Kahn. However, for nondeterministic networks, the straight-forward generalization…
We study the complexity of type inference for a core fragment of ML with lambda abstraction, function application, and the polymorphic let declaration. Our primary technical tool is the unification problem for a class of “polymorphic” type expressions. This form of unification, w…
Using concepts from denotational semantics, we have produced a very simple compiler that can be used to compile standard programming languages and produces object code as efficient as that of production compilers. The compiler is based entirely on source-to-source transformations…
We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm with a probability arbitrary clo…