A substantial amount of work has been devoted to the proof of correctness of various program analyses but much less attention has been paid to the correctness of compiler optimisations based on these analyses. In this paper we tackle the problem in the context of strictness analysis for lazy functional languages. We show that compiler optimisations based on strictness analysis can be expressed formally in the functional framework using continuations. This formal presentation has two benefits: it allows us to give a rigorous correctness proof of the optimised compiler; and it exposes the various optimisations made possible by a strictness analysis.

We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic extensions of it. The λ-calculus extended with surjective pairing has been well-studied in the last two decades. It is not confluent in the untyped case, and confluent in the typed case. But to the best of our knowledge the present work is the first treatment of the lambda calculus extended with surjective pairing and terminal object via a confluent rewriting system, and is the first solution to the decidability problem of the full equational theory of Cartesian Closed Categories extended with polymorphic types. Our approach yields conservativity results as well. In separate papers we apply our results to the study of provable type isomorphisms, and to the decidability of equality in a typed λ-calculus with subtyping.

We have developed a simple algebraic approach to music description and composition called Haskore. In this framework, musical objects consist of primitive notions such as notes and rests, operations to transform musical objects such as transpose and tempo-scaling, and operations to combine musical objects to form more complex ones, such as concurrent and sequential composition. When these simple notions are embedded into a functional language such as Haskell, rather complex musical relationships can be expressed clearly and succinctly. Exploiting the algebraic properties of Haskore, we have further defined a notion of literal performance (devoid of articulation) through which observationally equivalent musical objects can be determined. With this basis many useful properties can be proved, such as commutative, associative, and distributive properties of various operators. An algebra of music thus surfaces.

This paper makes a contribution to the refinement of systems which involve search by proposing a simple non-deterministic model for rule based transition systems and using this to define a meaning for rule based refinement which allows each stage of the software development path to be verified with respect to the previous stage. The proposal allows a system which involves search to be specified in terms of all the possible outcomes. Each stage of refinement will introduce complexity to the rules and therefore develop the search space in ever more sophisticated ways. At each stage of the refinement it will be possible to be precise about which collections of outcomes have been deleted, thereby achieving a verified (prototype) implementation.

The weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the implementation have been shown unsound, the concept has not been proved sound or unsound. We present an explanation of weak polymorphism and show that a formalization of this is sound. We also relate this to the SML/NJ implementation of weak polymorphism through a series of type systems that incorporate elements of the SML/NJ type inference algorithm.

We argue that the novel combination of type classes and existential types in a single language yields significant expressive power. We explore this combination in the context of higher-order functional languages with static typing, parametric polymorphism, algebraic data types and Hindley–Milner type inference. Adding existential types to an existing functional language that already features type classes requires only a minor syntactic extension. We first demonstrate how to provide existential quantification over type classes by extending the syntax of algebraic data type definitions, and give examples of possible uses. We then develop a type system and a type inference algorithm for the resulting language. Finally, we present a formal semantics by translation to an implicitly-typed second-order λ-calculus and show that the type system is semantically sound. Our extension has been implemented in the Chalmers Haskell B. system, and all examples from this paper have been developed using this system.

A combinator-based parser is a parser constructed directly from a BNF grammar, using higher-order functions (combinators) to model the alternative and sequencing operations of BNF. This paper describes a method for constructing parser combinators that can be used to build efficient predictive parsers which accurately report the cause of parsing errors. The method uses parsers that return values (parse trees or error indications) decorated with one of four tags.

This paper investigates several sparse matrix representation schemes and associated algorithms in Haskell for solving linear systems of equations arising from solving realistic computational fluid dynamics problems using a finite element algorithm. This work complements that of Wainwright and Sexton (1992) in that a Choleski direct solver (with an emphasis on its forward/backward substitution steps) is examined. Experimental evidence comparing time and space efficiency of these matrix representation schemes is reported, together with associated forward/backward substitution implementations. Our results are in general agreement with Wainwright and Sexton's.

A simple Idealized Algol is considered, based on Reynolds's ‘essence of Algol’. It is shown that observational equivalence in this language conservatively extends observational equivalence in its assignment-free functional sublanguage.

We present a short and direct syntactic proof of the fact that adding the axiom of choice and the principle of excluded-middle to Coquand–Huet's Calculus of Constructions gives proof-irrelevance.

This article describes the application of functional programming techniques to a problem previously studied by imperative programmers, that of drawing general trees automatically. We first consider the nature of the problem and the ideas behind its solution (due to Radack), independent of programming language implementation. We then describe a Standard ML program which reflects the structure of the abstract solution much better than an imperative language implementation. We conclude with an informal discussion on the correctness of the implementation and some changes which improve the algorithm's worst-case time complexity.