POPL

It is well known that adding side effects to functional languages changes the operational equivalences of the language. We develop a new language construct, encap, that forces imperative pieces of code to behave purely functionally, i.e.,without any ...

We call language L₁ intensionally more expressive than L₂ if there are functions which can be computed faster in L₁ than in L₂. We study the intensional expressiveness of several languages: the Berry-Curien programming language of sequential algorithms, ...

In the early 80's Oles and Reynolds devised a semantic model of Algol-like languages using a category of functors from a category of store shapes to the category of predomains. Here we will show how a variant of this idea can be used to define the ...

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 ...

The paper shows how a large class of interprocedural dataflow-analysis problems can be solved precisely in polynomial time by transforming them into a special kind of graph-reachability problem. The only restrictions are that the set of dataflow facts ...

Dataflow analysis framework based on Static Single Assignment (SSA) form and Sparse Evaluation Graphs (SEGs) demand fast computation of program points where data flow information must be merged, the so-called φ-nodes. In this paper, we present a ...

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 ...

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 ...

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 ...

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 ...

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.

Traditional techniques for implementing polymorphism use a universal representation for objects of unknown type. Often, this forces a compiler to use universal representations even if the types of objects are known. We examine an alternative approach ...

we present a variety of the Standard ML module system where parameterized abstract types (i.e. functors returning generative types) map provably equal arguments to compatible abstract types, instead of generating distinct types at each applications as ...

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 ...

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 ...

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 ...

We investigate implementation techniques arising directly from Girard's Geometry of Interaction semantics for Linear Logic, specifically for a simple functional programming language (PCF). This gives rise to a very simple, compact, compilation schema ...

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 ...

The goal of program transformation is to improve efficiency while preserving meaning. One of the best known transformation techniques is Burstall and Darlington's unfold-fold method. Unfortunately the unfold-fold method itself guarantees neither ...

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 ...

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 ...

In this paper we present substantially improved thread partitioning algorithms for modern implicitly parallel languages. We present a new block partitioning algorithm, separation constraint partitioning, which is both more powerful and more flexible ...

We extend the model of [SJG94b] to express strong time-outs (and pre-emption): if an event A does not happen through time t, cause event B to happen at time t. Such constructs arise naturally in practice (e.g. in modeling transistors) and are supported ...

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. ...

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 ...

Concurrent object-oriented programming (COOP) languages focus the abstraction and encapsulation power of abstract data types on the problem of concurrency control. In particular, pure fine-grained concurrent object-oriented languages (as opposed to ...

This paper introduces superoperators, an optimization technique for bytecoded interpreters. Superoperators are virtual machine operations automatically synthesized from smaller operations to avoid costly per-operation overheads. Superoperators decrease ...

We show how a set of building blocks can be used to construct programming language interpreters, and present implementations of such building blocks capable of supporting many commonly known features, including simple expressions, three different ...

Depth-first search is the key to a wide variety of graph algorithms. In this paper we express depth-first search in a lazy functional language, obtaining a linear-time implementation. Unlike traditional imperative presentations, we use the structuring ...