916 papers · page 36 of 46
Without adding any primitives to the language, we define a concurrency monad transformer in Haskell. This allows us to add a limited form of concurrency to any existing monad. The atomic actions of the new monad are lifted actions of the underlying monad. Some extra operations, s…
We derive a confluent λ-calculus with a catch/throw mechanism (called λ ct -calculus) from Parigot's λμ-calculus. We also present several translations from one calculus into the other which are morphisms for the reduction. We use them to show that the λ ct -calculus is a retract …
The future annotation of MultiLisp provides a simple method for taming the implicit parallelism of functional programs. Prior research on future has concentrated on implementation and design issues, and has largely ignored the development of a semantic characterization of future …
List homomorphisms are functions that are parallelizable using the divide-and-conquer paradigm. We study the problem of finding homomorphic representations of functions in the Bird–Meertens constructive theory of lists, by means of term rewriting and theorem proving techniques. A…
This paper is about point-free (or ‘pointless’) calculations – calculations performed at the level of function composition instead of that of function application. We address this topic with the help of an example, namely calculating the radix-sort algorithm from a more obvious s…
We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operati…
This paper discusses the principles of implementing an LCF-style proof assistant using a purely functional metalanguage. Two approaches are described; in both, signatures are treated as ordinary values, rather than as mutable components within an abstract datatype. The first appr…
Functional logic languages with a sound and complete operational semantics are mainly based on an inference rule called narrowing. Narrowing extends functional evaluation by goal solving capabilities, as in logic programming. Due to the huge search space of simple narrowing, stea…
The close relationship between writing programs and proving theorems has frequently been cited as an advantage of functional programming languages. We illustrate the interplay between programming and proving in the development of a program for regular expression matching. The pre…
We present a hierarchical classification of specializations of the divide-and-conquer paradigm. The aim is to identify a subclass of divide-and-conquer algorithms with an efficient parallel implementation which can be viewed as a static space-time mapping. The specializations imp…
Functional programming languages are an excellent tool for teaching algorithms and data structures. This paper explains binomial heaps, a beautiful data structure for priority queues, using the functional programming language Haskell (Peterson and Hammond, 1997). We largely follo…
This paper was guest-edited by Harry Mairson and Bruce Kapron, for our intended Special Issue on Functional Programming and Computational Complexity. Other papers submitted for the special issue were either out-of-scope or otherwise unsuitable for JFP. Even though only one paper …
In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the universal property of fold both as …
Proof by mathematical induction plays a crucial role in reasoning about functional programs. A generalization step often holds the key to discovering an inductive proof. We present a generalization technique which is particularly applicable when reasoning about functional program…
Recursive block decomposition algorithms (also known as quadtree algorithms when the blocks are all square) have been proposed to solve well-known problems such as matrix addition, multiplication, inversion, determinant computation, block LDU decomposition and Cholesky and QR fac…
The design of theorem provers, especially in the LCF-prover family, has strongly profited from functional programming. This paper attempts to develop a metaphor suited to visualize the LCF-style prover design, and a methodology for the implementation of graphical user interfaces …
Power series and stream processing were made for each other. Stream algorithms for power series are short, sweet, and compositional. Their neatness shines through in Haskell, thanks to pattern-matching, lazy lists, and operator overloading. In a short compass one can build workin…
HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF supports standard domain theory…
This article proposes a new language mechanism for data-parallel processing of dynamically allocated recursively defined data. Different from the conventional array-based data- parallelism, it allows parallel processing of general recursively defined data such as lists or trees i…
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 b…