916 papers · page 43 of 46
Abstract Self-applicable specializers have been used successfully to automate the generation of compilers. Specializers are often rather sophisticated, for which reason one would like to adapt and transform them with the aid of the computer. But how to automate this process? The …
Abstract We analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus ( F 2 ) invented by Girard and Reynolds, as well as higher-order extensions F 3 , F 4 , …, F ω proposed by Girard. We prove that recognising the…
Abstract 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 theor…
Abstract The Flagship Project 1 was a research collaboration between the University of Manchester, Imperial College London and International Computers Ltd. The project was unusual in that it aimed to produce a complete computing system based on a declarative programming style. Th…
Abstract In this paper we present an equivalence between TIM, a machine developed to implement non-strict functional programming languages, and the set of Categorical Multi-Combinators, a rewriting system developed with similar aims. These two models of computation at first appea…
Abstract Unfolding is a common technique in program transformations. Here, we present a computation model where unfolding is a simple generalisation of the usual concept of evaluation. The model is a variant of the well-known full substitution evaluation rule for recursive progra…
Abstract We take Abramsky's term assignment for Intuitionistic Linear Logic (the linear term calculus) as the basis of a functional programming language. This is a language where the programmer must embed explicitly the resource and control information of an algorithm. We give a …
Abstract 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 computa…
Abstract We develop a formal, type-theoretic account of the basic mechanisms of object-oriented programming: encapsulation, message passing, subtyping and inheritance. By modelling object encapsulation in terms of existential types instead of the recursive records used in other r…
Abstract In this paper we present a language for programming with higher-order modules. The language HML is based on Standard ML in that it provides structures, signatures and functors. In HML, functors can be declared inside structures and specified inside signatures; this is no…
Abstract This paper discusses the transformation power of Burstall and Darlington's folding/unfolding system, i.e. what kind of programs can be derived from a given one. A necessary condition of derivability is proved. The notion of inherent complexity of recursive functions in i…
Capsule ReviewIn late 1991 I organized an international programming competition for the Standard ML community.Each entrant implemented the 'set of integers' abstract data type, matching a signature that I provided.Prizes (donated by MIT Press) were awarded in two categories: fast…
Abstract Standard ML is an excellent language for many kinds of programming. It is safe, efficient, suitably abstract, and concise. There are many aspects of the language that work well. However, nothing is perfect: Standard ML has a few shortcomings. In some cases there are obvi…
Abstract In this paper we describe an implementation of an interactive version of the purely functional programming language Lazy ML (LML). The most remarkable fact about the interactive system is that it is written in a pure functional style using LML, yet the efficiency still c…
Abstract We describe the Edinburgh SML Library and draw lessons from its development. These lessons are of two kinds. The first concerns how to use SML to write a library, and shows some of the design choices that have to be considered. Most of the paper concerns this topic. The …
Abstract Based on Henglein's efficient binding-time analysis for the lambda calculus (with constants and ‘fix’) (Henglein, 1991), we develop three efficient analyses for use in the preprocessing phase of Similix, a self-applicable partial evaluator for a higher-order subset of Sc…
Abstract Pattern matching in modern functional programming languages is tied to the representation of data. Unfortunately, this is incompatible with the philosophy of abstract data types. Two proposals have been made to generalize pattern matching to a broader class of types. The…
Abstract This paper provides a formal treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. The results obtained make less justified the commonplace feeling that (the core of) ML is a subset of second order λ-calculus: we can …