POPL

This paper explores the use monads to structure functional programs. No prior knowledge of monads or category theory is required.

Monads increase the ease with which programs may be modified. They can mimic the effect of impure features such as exceptions, ...

Lamping discovered an optimal graph-reduction implementation of the λ-calculus. Simultaneously, Girard invented the geometry of interaction, a mathematical foundation for operational semantics. In this paper, we connect and explain the geometry of ...

We present a functional interpretation of classical linear logic based on the concept of linear continuations. Unlike their non-linear counterparts, such continuations lead to a model of control that does not inherently impose any particular evaluation ...

Distributed symbolic computations involve the existence of remote references allowing an object, local to a processor, to designate another object located on another processor. To reclaim inaccessible objects is the non trivial task of a distributed ...

Our research is concerned with compiler-independent, tag-free garbage collection for the C++ programming language. We have previously presented a copying collector based on root registration. This paper presents a mark-and-sweep garbage collector that ...

This paper presents algorithms for inserting monitoring code to profile and trace programs. These algorithms greatly reduce the cost of measuring programs. Profiling counts the number of times each basic block in a program executes and has a variety of ...

In the context of abstract interpretation we study the number of times a functional need to be unfolded in order to give the least fixed point. For the cases of the total or monotone functions we obtain an exponential bound and in the case of strict and ...

We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can ...

The goal of this paper is to construct a semantic basis for the abstract interpretaion of Prolog programs. Prolog is a well-known logic programming language which applies a depth-first search strategy in order to provide a practical approximation of ...

Jade is a language designed to support coarse-grain parallelism on both shared and distributed address-space machines. Jade is data-oriented: a Jade programmer simply augments a sequential imperative program with declarations specifying how the program ...

We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define ...

Traditional optimization techniques for sequential programs are not directly applicable to parallel programs where concurrent activities may interfere with each other through shared variables. New compiler techniques must be developed to accommodate ...

We present a taxonomy of languages for multiparty interaction, which covers all proposals of which we are aware. Based on this taxonomy, we present a comprehensive analysis of the computational complexity of the multiparty interaction implementation ...

Polymorphic record calculi have recently attracted much attention as a typed foundation for object-oriented programming. This is based on the fact that a function that selects a field l of a record can be given a polymorphic type that enables it to be ...

We show that any functional language with record extension possesses record concatenation for free. We exhibit a translation from the latter into the former. We obtain a type system for a language with record concatenation by composing the translation ...

This paper presents a program transformation that allows languages with polymorphic typing (e.g. ML) to be implemented with unboxed, multi-word data representations. The transformation introduces coercions between various representations, based on a ...

Under the Damas-Milner type discipline for functional languages, every expression has principal type, if it elaborates at all. In the type discipline for ML Modules, a signature expression has a principal signature, if it elaborates at all. However, ...

This paper contains a full treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. Surprisingly enough the results obtained contradict the common-place feeling that (the core of) ML is a subset of ...

Attribute grammars have been used for many language-oriented tasks, including the formal description of semantics and the implementation of compilation tasks from simple type checking through code generation. Despite their successful use, attribute ...

This paper introduces Composable Attribute Grammars (CAGs), a formalism that extends classical attribute grammars to allow for the modular composition of translation specifications and of translators. CAGs bring to complex translator writing systems the ...

LR parsing techniques have long been studied as efficient and powerful methods for processing context free languages. A linear time algorithm for recognizing languages representable by LR(k) grammars has long been known. Recognizing substrings of a ...

The notion of dominators is generalized to include multiple-vertex dominators in addition to single-vertex dominators. A multiple-vertex dominator of a vertex is a group of vertices that collectively dominate the vertex. Existing algorithms compute ...

Compiler generation is often emphasized as being the most important application of partial evaluation. But most of the larger practical applications have, to the best of our knowledge, been outside this field. Expecially, no one has generated compilers ...

A polymorphic function is parametric if it has uniform behavior for all type parameters. This property is useful when writing, reasoning about, and compiling functional programs.

We show how to syntactically define and reason about parametricity in a ...

We study the complexity of type inference for programming languages with subtypes. There are three language variations that effect the problem: (i) basic functions may have polymorphic or more limited types, (ii) the subtype hierarchy may be fixed or ...

F≤ is a typed λ-calculus with subtyping and bounded second-order polymorphism. First proposed by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping.

Curien and Ghelli proved the partial correctness of a ...

One of the major challenges in denotational semantics is the construction of fully abstract models for sequential programming languages. For the past fifteen years, research on this problem has focused on developing models for PCF, an idealized ...

We describe a method for using abstraction to reduce the complexity of temporal logic model checking. The basis of this method is a way of constructing an abstract model of a program without ever examining the corresponding unabstracted model. We show ...