916 papers · page 39 of 46
In this paper we investigate the effectiveness of functional language features when writing scientific codes. Our programs are written in the purely functional subset of Id and executed on a one node Motorola Monsoon machine, and in Haskell and executed on a Sparc 2. In the appli…
Thirty-five years ago, thunks were used to simulate call-by-name under call-by-value in Algol 60. Twenty years ago, Plotkin presented continuation-based simulations of call-by-name under call-by-value and vice versa in the λ-calculus. We connect all three of these classical simul…
While the quality of the results of T E X's mathematical formula layout algorithm is convincing, its original description is hard to understand since it is presented as an imperative program with complex control flow and destructive manipulations of the data structures representi…
Almost every programmer has faced the problem of representing a tree together with a subtree that is the focus of attention, where that focus may move left, right, up or down the tree. The Zipper is Huet's nifty name for a nifty data structure which fulfills this need. I wish I h…
N ATURAL E XPERT is a product that allows users to build knowledge-based systems. It uses a lazy functional language, N ATURAL E XPERT L ANGUAGE , to implement backward chaining and provide a reliable knowledge processing environment in which development can take place. Customers…
We present narrowing calculi that are computation models of functional-logic programming languages. The narrowing calculi are based on the notion of the leftmost outside-in reduction of Huet and Lévy. We note the correspondence between the narrowing and reduction derivations, and…
The last 15 years have seen an explosion in work on explicit substitution, most of which is done in the style of the λσ-calculus. In Kamareddine and Ríos (1995a), we extended the λ-calculus with explicit substitutions by turning de Bruijn's meta-operators into object-operators of…
This paper describes E QUALS , a fast parallel implementation of a lazy functional language on a commercially available shared-memory parallel machine, the Sequent Symmetry. In contrast to previous implementations, we propagate normal form demand at compile time as well as run ti…
Arrays are probably the most widely used data structure in imperative programming languages, yet functional languages typically only support arrays in a limited manner, or prohibit them entirely. This is not too surprising, since most other mutable data structures, such as trees,…
Among the many flavours of balanced binary trees, Braun trees (Braun and Rem, 1983) are perhaps the most circumscribed. For any given node of a Braun tree, the left subtree is either exactly the same size as the right subtree, or one element larger. Braun trees always have minimu…
This paper introduces trust analysis for higher-order languages. Trust analysis encourages the programmer to make explicit the trustworthiness of data, and in return it can guarantee that no mistakes with respect to trust will be made at run-time. We present a confluent λ-calculu…
The purpose of this paper is to demonstrate that first-order functional programs can be transformed into intensional programs of nullary variables, in a semantics preserving way. On the foundational side, the goal of our study is to bring new insights and a better understanding o…
The popular method of enumerating the primes is the Sieve of Eratosthenes . It can be programmed very neatly in a lazy functional language, but runs rather slowly. A little-known alternative method is the Wheel Sieve , originally formulated as a fast imperative algorithm for obta…
We derive a simple abstract machine for lazy evaluation of the lambda calculus, starting from Launchbury's natural semantics. Lazy evaluation here means non-strict evaluation with sharing of argument evaluation, i.e. call-by-need. The machine we derive is a lazy version of Krivin…
Abstract We present a comprehensive analysis of all the components of creation, access and disposal of heap-allocated and stack-allocated activation records. Among our results are: •Although stack frames are known to have a better cache read-miss rate than heap frames, our simple…
Abstract The Bologna Optimal Higher-order Machine (BOHM) is a prototype implementation of the core of a functional language based on (a variant of) Lamping's optimal graph reduction technique (Lamping, 1990; Gonthier et al. , 1992a; Asperti, 1994). The source language is a sugare…
Abstract 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.
Abstract Explicit substitutions were proposed by Abadi, Cardelli, Curien, Hardin and Lévy to internalise substitutions into λ-calculus and to propose a mechanism for computing on substitutions. λν is another view of the same concept which aims to explain the process of substituti…
Capsule ReviewIt had been known that the simplest system with dependent types, XP, is undecidable, in that sense that the set {(A,D\3pr\-XP p:A} is non-computable.The proof runs as follows.First, there is an obvious embedding of predicate logic into XP.This is the principle idea …
Abstract A generic functional program is one which is parameterised by datatype. By installing specific choices, for example lists or trees, different programs are obtained that are, nevertheless, abstractly the same. The purpose of this paper is to explore the possibility of der…