916 papers · page 21 of 46
Abstract Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Moreover, the argument types of the constructors refer to indices given by expressions in which the f…
This special issue of the Journal of Functional Programming collects revised selected articles arising from the inaugural meeting of the Workshop on Mathematically Structured Functional Programming, MSFP 2006, held in Kuressaare, Estonia, on 2 July 2006, with support from the Eur…
Abstract Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties…
Abstract We present natural semantics for acyclic as well as cyclic call-by-need lambda calculi, which are proved equivalent to the reduction semantics given by Ariola and Felleisen ( J. Funct. Program. , vol. 7, no. 3, 1997). The natural semantics are big-step and use global hea…
Abstract A much beloved and widely used example showing the elegance and simplicity of lazy functional programming represents itself as “The Sieve of Eratosthenes.” This paper shows that this example is not the sieve and presents an implementation that actually is.
Abstract Regular-expression derivatives are an old, but elegant, technique for compiling regular expressions to deterministic finite-state machines. It easily supports extending the regular-expression operators with boolean operations, such as intersection and complement. Unfortu…
Abstract As a means of transmitting not only data but also code encapsulated within functions, higher-order channels provide an advanced form of task parallelism in parallel computations. In the presence of mutable references, however, they pose a safety problem because reference…
Abstract Macros still haven't made their way into typed higher-order programming languages such as Haskell and Standard ML. Therefore, to extend the expressiveness of Haskell or Standard ML, one must express new linguistic features in terms of functions that fit within the static…
Abstract A constraint programming system combines two essential components: a constraint solver and a search engine. The constraint solver reasons about satisfiability of conjunctions of constraints, and the search engine controls the search for solutions by iteratively exploring…
Abstract One approach to give semantics to languages with subtypes is by translation to target languages without subtyping: subtypings A ≤ B are interpreted via conversion functions A → B . This paper shows how to extend the method to languages with computational effects, using M…
Abstract Combinatorial search strategies including depth-first, breadth-first and depth-bounded search are shown to be different implementations of a common algebraic specification that emphasizes the compositionality of the strategies. This specification is placed in a categoric…
Abstract We present two implementations of Oppen's pretty-printing algorithm in Haskell that meet the efficiency of Oppen's imperative solution but have a simpler and a clear structure. We start with an implementation that uses lazy evaluation to simulate two co-operating process…
Abstract We combine ideas from types for continuations, effect systems and monads in a very simple setting by defining a version of classical propositional logic in which double-negation elimination is combined with a modality. The modality corresponds to control effects, and it …
Abstract Experimental game theory is increasingly important for research in many fields. Unfortunately, it is poorly supported by computer tools. We have created Hagl, a domain-specific language embedded in Haskell, to reduce the development time of game-theoretic experiments and…
Abstract The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a continuation. To the contrary, the control calculus, developed by the authors, …
Abstract Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. …
Abstract This paper introduces a pattern for almost compositional functions over recursive data types, and over families of mutually recursive data types. Here “almost compositional” means that for all of the constructors in the type(s), except a limited number of them, the resul…