916 papers · page 37 of 46
In this paper we demonstrate that a broad class of higher-order functional programs can be transformed into semantically equivalent multidimensional intensional programs that contain only nullary variable definitions. The proposed algorithm systematically eliminates user-defined …
This theoretical pearl is about the closed term model of pure untyped lambda-terms modulo β-convertibility. A consequence of one of the results is that for arbitrary distinct combinators (closed lambda terms) M , M ′, N , N ′ there is a combinator H such that formula here The gen…
We present a general method to transform a compositional specification of a specializer for a functional programming language into a set of combinators that can be used to perform the same specialization more efficiently. The main transformation steps are the transition to higher…
In this paper, we show how lazy functional programs can be compiled for the Java Virtual Machine using a mapping between a version of the 〈 v , G 〉-machine and the Java Virtual Machine. This mapping is elegant – the description is entirely straightforward – and efficient – using …
Moggi's computational lambda calculus is a metalanguage for denotational semantics which arose from the observation that many different notions of computation have the categorical structure of a strong monad on a cartesian closed category. In this paper we show that the computati…
Meertens number is a number with a very peculiar property. I had the idea in 1991, when I was invited to celebrate the occasion of Lambert Meertens' 25 years at the CWI, Amsterdam. Lambert has been a good friend and colleague for a number of years, and rather than bring the usual…
A string-formatting function such as printf in C seemingly requires dependent types, because its control string determines the rest of its arguments. Examples: formula here We show how changing the representation of the control string makes it possible to program printf in ML (wh…
In this paper we describe the discrete interval encoding tree for storing subsets of types having a total order and a predecessor and a successor function. In the following, we consider for simplicity only the case for integer sets; the generalization is not difficult. The discre…
Concurrent ML (CML) is an extension of Standard ML of New Jersey with concurrent features similar to those of process algebra. In this paper, we build upon John Reppy's reduction semantics for CML by constructing a compositional operational semantics for a fragment of CML, based …
An important issue faced by implementors of higher-order functional programming languages is the allocation and deallocation of storage for variables. The possibility of variables escaping their scope during runtime makes traditional stack allocation inadequate. We consider the p…
We define a weak λ-calculus, λσ w , as a subsystem of the full λ-calculus with explicit substitutions λσ [uArr ] . We claim that λσ w could be the archetypal output language of functional compilers, just as the λ-calculus is their universal input language. Furthermore, λσ [uArr ]…
In type theory a proposition is represented by a type, the type of its proofs. As a consequence, the equality relation on a certain type is represented by a binary family of types. Equality on a type may be conventional or inductive. Conventional equality means that one particula…
In this paper we give a big-step Structured Operational Semantics (SOS), in the style of Plotkin, Kahn and Milner, of a significant fragment of the functional programming language Scheme , including quote, eval, quasiquote and unquote. The SOS formalism allows us to discuss incre…
This paper is a tutorial on defining recursive descent parsers in Haskell. In the spirit of one-stop shopping , the paper combines material from three areas into a single source. The three areas are functional parsers (Burge, 1975; Wadler, 1985; Hutton, 1992; Fokker, 1995), the u…
Unification, or two-way pattern matching, is the process of solving an equation involving two first-order terms with variables. Unification is used in type inference in many programming languages and in the execution of logic programs. This means that unification algorithms have …
We present an extension of the Hindley–Milner type system that supports a generous class of type constructors called functors, and provide a parametrically polymorphic algorithm for their mapping, i.e. for applying a function to each datum appearing in a value of constructed type…
Many, perhaps even most, algorithms that involve data structures are traditionally expressed by incremental updates of the data structures. In functional languages, however, incremental updates are usually both clumsy and inefficient, especially when the data structure is an arra…
We show the design principles of an automatic indentation GNU Emacs mode for Haskell and Miranda(tm), functional languages using the ‘layout rule’ instead of the usual parenthetic structures for indentifying dependent program parts.
We present a calculus that captures the operational semantics of call-by-need. The call-by-need lambda calculus is confluent, has a notion of standard reduction, and entails the same observational equivalence relation as the call-by-name calculus. The system can be formulated wit…
In this paper we aim to give an introduction to fuzzy logic using the language Haskell to implement our solutions. We shall see how the high-level, declarative nature of a functional language allows us to implement easily and efficiently solutions to problems using fuzzy logic an…