7,482 papers · page 306 of 375
this paper, we present an almost linear time algorithm to construct the GSA. The new algorithm is more efficient and simpler than the existing algorithms for GSA construction [BMO90, Hav93]. Since SSA is a special case of GSA, it can also be used as an efficient alternative algor…
This paper proposes an efficient technique for context-sensitive pointer analysis that is applicable to real C programs. For efficiency, we summarize the effects of procedures using partial transfer functions. A partial transfer function (PTF) describes the behavior of a procedur…
The paper presents methods that we have implemented to improve the quality of the def-uses reported for dynamically allocated locations. The methods presented are based on the Ruggieri/Murtagh naming scheme for dynamically created locations. We expand upon this scheme to name dyn…
The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct …
Procedure calling conventions are used to provide uniform procedure-call interfaces. Applications, such as compilers and debuggers, which generate, or process procedures at the machine-language abstraction level require knowledge of the calling convention. In this paper, we devel…
The programming language Standard ML provides first-order functors, i.e. modules parameterized by modules. First-order functors in the language have a simple and elegant static semantics. The type structure of higher-order modules, i.e. modules parameterized by functors, is well …
Standard specification languages have very limited abilities to define new operations on processes. We introduce the concept of a Protean specification language, with general definitional facilities supported by the appropriate theory. Protean languages allow elegant, readable, a…
We investigate the verification problem of infinite-state process w.r.t. logic-based specifications that express properties which may be nonregular. We consider the process algebra PA which integrates and strictly subsumes the algebras BPA (basic process algebra) and BPP (basic p…
We call language L1 intensionally more expressive than L2 if there are functions which can be computed faster in L1 than in L2. We study the intensional expressiveness of several languages: the Berry-Curien programming language of sequential algorithms, CDS0, a deterministic para…
Obliq is a lexically-scoped, untyped, interpreted language that supports distributed object-oriented computation. Obliq objects have state and are local to a site. Obliq computations can roam over the network, while maintaining network connections. Distributed lexical scoping is …
No abstract available.
The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smalle…
We present the extensional polymorphism, a framework to type check ad hoc polymorphic functions. This formalism is compatible with parametric polymorphism, and supports a large class of functions defined by structural pattern matching on types.
This paper presents a general framework for deriving demand-driven algorithms for interprocedural data flow analysis of imperative programs. The goal of demand-driven analysis is to reduce the time and/or space overhead of conventional exhaustive analysis by avoiding the collecti…
The ring is a useful means of structuring concurrent processes. Processes communicate by passing a token in a fixed direction; the process that possesses the token is allowed to make certain moves. Usually, correctness properties are expected to hold irrespective of the size of t…
Program slicing is a technique for isolating computational threads in programs. In this paper, we show how to mechanically extract a family of practical algorithms for computing slices directly from semantic specifications. These algorithms are based on combining the notion of dy…
The future annotations of MultiLisp provide a simple method for taming the implicit parallelism of functional programs. Past research concerning futures has focused on implementation issues. In this paper, we present a series of operational semantics for an idealized functional l…
The views and conclusions contained in this document are those of the authors and should not be interpreted as
We investigate type inference for programming languages with subtypes. As described in previous work, there are several type inference problems for any given expression language, depending on the form of the subtype partial order and the ability to define new subtypes in programs…
The statement S≤T in a λ-calculus with subtyping is traditionally interpreted by a semantic coercion function of type [[S]]→[[T]] that extracts the “T part” of an element of S. If the subtyping relation is restricted to covariant positions, this interpretation may be enriched to …