Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages—languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the “semantic cube”: fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences.

In this paper, we marry the aspirations of the semantic cube to the powerful proof method of step-indexed Kripke logical relations. Building on recent work of Ahmed et al. (2009), we define the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power of our language—namely, the restriction to first-order state and/or the removal of call/cc—we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of state transition systems to model the way in which properties of local state evolve over time.

A method is proposed to search for an identifier in a functional program library by using its Hindley–Milner type as a key. This can be seen as an approximation of using the specification as a key.

Functions that only differ in their argument order or currying are essentially the same, which is expressed by a congruence relation on types. During a library search, congruent types are identified. If a programmer is not satisfied with the type of a found value, he can use a conversion function (like curry), which must exist between congruent types, to convert the value into the type of his choice.

Types are congruent if they are isomorphic in all cartesian closed categories. To put it more simply, types are congruent if they are equal under an arithmetical interpretation, with cartesian product as multiplication and function space as exponentiation. This congruence relation is characterized by seven equational axioms. There is a simple term-rewriting algorithm to decide congruence, using which a search system has been implemented for the functional language Lazy ML, with good performance.

The congruence relation can also be used as a basis for other search strategies, e.g. searching for identifiers of a more general type, modulo congruence or allowing free type variables in queries.

We propose a new style of writing graph algorithms in functional languages which is based on an alternative view of graphs as inductively defined data types. We show how this graph model can be implemented efficiently, and then we demonstrate how graph algorithms can be succinctly given by recursive function definitions based on the inductive graph view. We also regard this as a contribution to the teaching of algorithms and data structures in functional languages since we can use the functional-style graph algorithms instead of the imperative algorithms that are dominant today.

This paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes—a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.

The Iterator pattern gives a clean interface for element-by-element access to a collection, independent of the collection's shape. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various existing functional models of iteration capture one or other of these aspects, but not both simultaneously. We argue that C. McBride and R. Paterson's applicative functors (Applicative programming with effects, J. Funct. Program., 18 (1): 1–13, 2008), and in particular the corresponding traverse operator, do exactly this, and therefore capture the essence of the Iterator pattern. Moreover, they do so in a way that nicely supports modular programming. We present some axioms for traversal, discuss modularity concerns and illustrate with a simple example, the wordcount problem.

Many modern programming languages support basic generics, sufficient to implement type-safe polymorphic containers. Some languages have moved beyond this basic support, and in doing so have enabled a broader, more powerful form of generic programming. This paper reports on a comprehensive comparison of facilities for generic programming in eight programming languages: C++, Standard ML, Objective Caml, Haskell, Eiffel, Java, C# (with its proposed generics extension), and Cecil. By implementing a substantial example in each of these languages, we illustrate how the basic roles of generic programming can be represented in each language. We also identify eight language properties that support this broader view of generic programming: support for multi-type concepts, multiple constraints on type parameters, convenient associated type access, constraints on associated types, retroactive modeling, type aliases, separate compilation of algorithms and data structures, and implicit argument type deduction for generic algorithms. We find that these features are necessary to avoid awkward designs, poor maintainability, and painfully verbose code. As languages increasingly support generics, it is important that language designers understand the features necessary to enable the effective use of generics and that their absence can cause difficulties for programmers.

The worker/wrapper transformation is a technique for changing the type of a computation, usually with the aim of improving its performance. It has been used by compiler writers for many years, but the technique is little known in the wider functional programming community, and has never been described precisely. In this article we explain, formalise and explore the generality of the worker/wrapper transformation. We also provide a systematic recipe for its use as an equational reasoning technique for improving the performance of programs, and illustrate the power of this recipe using a range of examples.

Everybody learns about balanced binary search trees in their introductory computer science classes, but even the stouthearted tremble at the thought of actually implementing such a beast. The details surrounding rebalancing are usually just too messy. To show that this need not be the case, we present an algorithm for insertion into red-black trees (Guibas and Sedgewick, 1978) that any competent programmer should be able to implement in fifteen minutes or less.

The increasing availability of commodity multicore processors is making parallel computing ever more widespread. In order to exploit its potential, programmers need languages that make the benefits of parallelism accessible and understandable. Previous parallel languages have traditionally been intended for large-scale scientific computing, and they tend not to be well suited to programming the applications one typically finds on a desktop system. Thus, we need new parallel-language designs that address a broader spectrum of applications. The Manticore project is our effort to address this need. At its core is Parallel ML, a high-level functional language for programming parallel applications on commodity multicore hardware. Parallel ML provides a diverse collection of parallel constructs for different granularities of work. In this paper, we focus on the implicitly threaded parallel constructs of the language, which support fine-grained parallelism. We concentrate on those elements that distinguish our design from related ones, namely, a novel parallel binding form, a nondeterministic parallel case form, and the treatment of exceptions in the presence of data parallelism. These features differentiate the present work from related work on functional data-parallel language designs, which have focused largely on parallel problems with regular structure and the compiler transformations—most notably, flattening—that make such designs feasible. We present detailed examples utilizing various mechanisms of the language and give a formal description of our implementation.

Lazy functional languages have non-strict semantics and are purely declarative, i.e. they support the notion of referential transparency and are devoid of side-effects. Traditional debugging techniques are, however, not suited for lazy functional languages, since computations generally do not take place in the order one might expect. Since algorithmic debugging allows the user to concentrate on the declarative aspects of program semantics, and will semi-automatically find functions containing bugs, we propose to use this technique for debugging lazy functional programs. Because of the non-strict semantics of lazy functional languages, arguments to functions are in general partially evaluated expressions. The user is, however, usually more concerned with the values that these expressions represent. We address this problem by providing the user with a strictified view of the execution trace whenever possible. In this paper, we present an algorithmic debugger for a lazy functional language based on strictification and some experience in using it. A number of problems with the current implementation of the debugger (e.g. too large trace size and too many questions asked) are also discussed and some techniques for overcoming these problems, at least partially, are suggested. The key techniques are immediate strictification and piecemeal tracing.

Functional programming languages have banned assignment because of its undesirable properties. The reward of this rigorous decision is that functional programming languages are side-effect free. There is another side to the coin: because assignment plays a crucial role in Input/Output (I/O), functional languages have a hard time dealing with I/O. Functional programming languages have therefore often been stigmatised as inferior to imperative programming languages because they cannot deal with I/O very well. In this paper, we show that I/O can be incorporated in a functional programming language without loss of any of the generally accepted advantages of functional programming languages. This discussion is supported by an extensive account of the I/O system offered by the lazy, purely functional programming language Clean. Two aspects that are paramount in its I/O system make the approach novel with respect to other approaches. These aspects are the technique of explicit multiple environment passing, and the Event I/O framework to program Graphical User I/O in a highly structured and high-level way. Clean file I/O is as powerful and flexible as it is in common imperative languages (one can read, write, and seek directly in a file). Clean Event I/O provides programmers with a high-level framework to specify complex Graphical User I/O. It has been used to write applications such as a window-based text editor, an object based drawing program, a relational database, and a spreadsheet program. These graphical interactive programs are completely machine independent, but still obey the look-and-feel of the concrete window environment being used. The specifications are completely functional and make extensive use of uniqueness typing, higher-order functions, and algebraic data types. Efficient implementations are present on the Macintosh, Sun (X Windows under Open Look) and PC (OS/2).

Inspired by the continuation-passing encoding of binary sessions, we describe a simple approach to embed a hybrid form of session type checking into any programming language that supports parametric polymorphism. The approach combines static protocol analysis with dynamic linearity checks. To demonstrate the effectiveness of the technique, we implement a well-integrated OCaml module for session communications. For free, OCaml provides us with equirecursive session types, parametric behavioural polymorphism, complete session type inference, and session subtyping.

Staging is a programming technique for dividing the computation in order to exploit the early availability of some arguments. In the early stages the program uses the available arguments to generate, at run time, the code for the late stages. A type system for staging should ensure that only well-typed expressions are generated, and that only expressions with no free variables are permitted for evaluation. In this paper, we present a calculus for staged computation in which code from the late stages is composed by splicing smaller code fragments into a larger context, possibly incurring capture of free variables. The type system ensures safety by tracking the names of free variables for each code fragment. The type system is based on the necessity operator □ from constructive modal logic, which we index with a set of names C. Our type □CA classifies expressions of type A that belong to the late stage, and whose free names are in the set C.

This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so-called event traces. Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the λ-calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the trace effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain trace event checks that can fail at run-time.

A new program transformation method is presented. It is a further refinement of supercompilation where the supercompiler is not applied directly to the function to be transformed, but to a metafunction, namely an interpreter which computes this function using its definition and an abstract (i.e. including variables) input. It is shown that with this method such tranformations become possible which the direct application of the supercompiler cannot perform. Examples include the merging of iterative loops, function inversion, and transformation of deterministic into non-deterministic algorithms, and vice-versa.

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types (Honda et al., 1998). However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions (Clarke & Marrero, 1998; Gordon & Jeffrey, 2003b). The resulting type discipline augments the types of long-term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. This new type system can be used to check:

1. source of information,

2. whether data is propagated as specified across multiple parties,

3. if there are unspecified communications between parties, and

4. if the data being exchanged has been modified by the code in an unspecified way.

This paper presents STAL, a variant of Typed Assembly Language with constructs and types to support a limited form of stack allocation. As with other statically-typed low-level languages, the type system of STAL ensures that a wide class of errors cannot occur at run time, and therefore the language can be adapted for use in certifying compilers where security is a concern. Like the Java Virtual Machine Language (JVML), STAL supports stack allocation of local variables and procedure activation records, but unlike the JVML, STAL does not pre-suppose fixed notions of procedures, exceptions, or calling conventions. Rather, compiler writers can choose encodings for these high-level constructs using the more primitive RISC-like mechanisms of STAL. Consequently, some important optimizations that are impossible to perform within the JVML, such as tail call elimination or callee-saves registers, can be easily expressed within STAL.

Objects with dynamic types allow the integration of operations that essentially require runtime type-checking into statically-typed languages. This paper presents two extensions of the ML language with dynamics, based on our work on the CAML implementation of ML, and discusses their usefulness. The main novelty of this work is the combination of dynamics with polymorphism.

From the points of view of programming pragmatics, rewriting and operational semantics, the syntactic construct used for exception handling in ML-like programming languages, and in much theoretical work on exceptions, has subtly undesirable features. We propose and discuss a more well-behaved construct.

We present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms). Gallina is the specification language of the Coq Proof Assistant (Dowek et al., 1991; Huet 1992b). It is a specific concrete syntax for its abstract framework, the Calculus of Inductive Constructions (Paulin-Mohring, 1993). It may be thought of as a smooth mixture of higher-order predicate calculus with recursive definitions, inductively defined data types and inductive predicate definitions reminiscent of logic programming. The development presented here was fully checked in the current distribution version Coq V5.8. We just state the lemmas in the order in which they are proved, omitting the proof justifications. The full transcript is available as a standard library in the distribution of Coq.