2,199 papers · page 93 of 110
The model theory of simply typed and polymorphic (second-order) lambda calculus changes when types are allowed to be empty. For example, the “polymorphic Boolean” type really has exactly two elements in a polymorphic model only if the “absurd” type ∀t.t is empty. The standard β-ε…
We provide a scheme for determining which global variables are involved when an expression is evaluated in a language with higher order constructs and imperative features. The heart of our scheme is a mechanism for computing the support of an expression, i.e. the set of global va…
A theory of abstract interpretation [CoCo79] is developed for a typed λ-calculus. The typed λ-calculus is the “static” part of a two-level denotational metalanguage for which abstract interpretation was developed in [Nie86]. The present development relaxes a condition imposed in …
Article Free Access Share on Semantics for concurrency without powerdomains Author: F. J. Oles Mathematical Sciences Department, IBM Thomas J. Watson Research Center, Yorktown Heights, New York Mathematical Sciences Department, IBM Thomas J. Watson Research Center, Yorktown Heigh…
In this paper we present some of the control constructs of the language CP, which is based on a concurrent interpretation of Horn logic programming. We present a formal structural operational semantics and relate the meaning of programs in this language to the underlying (pure) H…
Using concurrent transition systems [Sta86], we establish connections between three models of concurrent process networks, Kahn functions, input/output automata, and labeled processes. For each model, we define three kinds of algebraic operations on processes: the product operati…
In programming languages of universal power, the computational integers must be distinguished from the classical integers because of the “divergent” integer. Even the equational theory corresponding to evaluation of integer expressions is distinct from the theory of classical int…
Pattern matching and dta abstraction are important concepts in designing programs, but they do not it well together. Pattern matching depend on making public a free data type mpresentaiion, while data abstraction depends on hiding the repreentaiion. This paper proposes the vdws m…
Abstract. Most trace-based proof systems for networks of processes are known to be incomplete. Extensions to achieve completeness are generally complicated and cumbersome. In this paper, a simple trace logic is defined and two examples are presented to show its inherent incomplet…
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 throug…
The Centre for Mathematics and Computer
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 settin…
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 si…
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 pa…
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 optim…
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…
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,…
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 …
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 …