title: Weaving a web

authors:
Ralf Hinze
Johan Jeuring

abstract: Suppose, you want to implement a structured editor for some term type, so that the user can navigate through a given term and perform edit actions on subterms. In this case you are immediately faced with the problem of how to keep track of the cursor movements and the user's edits in a reasonably efficient manner. In a previous pearl, Huet (1997) introduced a simple data structure, the Zipper , that addresses this problem – we will explain the Zipper briefly in section 2. A drawback of the Zipper is that the type of cursor locations depends on the structure of the term type, i.e. each term type gives rise to a different type of location (unless you are working in an untyped environment). In this pearl, we present an alternative data structure, the web , that serves the same purpose, but that is parametric in the underlying term type. Sections 3–6 are devoted to the new data structure. Before we unravel the Zipper and explore the web, let us first give a taste of their use.


venue: jfp

title: On characterizations of the basic feasible functionals (Part I)

authors:
Robert J. Irwin
James S. Royer
Bruce M. Kapron

abstract: We introduce a typed programming formalism, type-2 inflationary tiered loop programs or ITLP 2 , that characterizes the type-2 basic feasible functionals. ITLP 2 is based on Bellantoni and Cook's (1992) and Leivant's (1995) type-theoretic characterization of polynomial-time, and turns out to be closely related to Kapron and Cook's (1991; 1996) machine-based characterization of the type-2 basic feasible functionals.


title: The expressive power of higher-order types or, life without CONS

abstract: Compare first-order functional programs with higher-order programs allowing functions as function parameters. Can the the first program class solve fewer problems than the second? The answer is no: both classes are Turing complete , meaning that they can compute all partial recursive functions. In particular, higher-order values may be first-order simulated by use of the list constructor ‘cons’ to build function closures. This paper uses complexity theory to prove some expressivity results about small programming languages that are less than Turing complete. Complexity classes of decision problems are used to characterize the expressive power of functional programming language features. An example: second-order programs are more powerful than first-order, since a function f of type [Bool]-〉Bool is computable by a cons-free first-order functional program if and only if f is in PTIME , whereas f is computable by a cons-free second-order program if and only if f is in EXPTIME . Exact characterizations are given for those problems of type [Bool]-〉Bool solvable by programs with several combinations of operations on data: presence or absence of constructors; the order of data values: 0, 1, or higher; and program control structures: general recursion, tail recursion, primitive recursion.


title: Red-black trees with types

abstract: Chris Okasaki showed how to implement red-black trees in a functional programming language. Ralf Hinze incorporated even the invariants of such data structures into their types, using higher-order nested datatypes. We show how one can achieve something very similar without the usual performance penalty of such types, by combining the features of nested datatypes, phantom types and existential type variables.


title: Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories

authors:
Hélène Kirchner
Pierre-Etienne Moreau

abstract: First-order languages based on rewrite rules share many features with functional languages, but one difference is that matching and rewriting can be made much more expressive and powerful by incorporating some built-in equational theories. To provide reasonable programming environments, compilation techniques for such languages based on rewriting have to be designed. This is the topic addressed in this paper. The proposed techniques are independent from the rewriting language, and may be useful to build a compiler for any system using rewriting modulo Associative and Commutative (AC) theories. An algorithm for many-to-one AC matching is presented, that works efficiently for a restricted class of patterns. Other patterns are transformed to fit into this class. A refined data structure, namely compact bipartite graph, allows encoding of all matching problems relative to a set of rewrite rules. A few optimisations concerning the construction of the substitution and of the reduced term are described. We also address the problem of non-determinism related to AC rewriting, and show how to handle it through the concept of strategies. We explain how an analysis of the determinism can be performed at compile time, and we illustrate the benefits of this analysis for the performance of the compiled evaluation process. Then we briefly introduce the ELAN system and its compiler, in order to give some experimental results and comparisons with other languages or rewrite engines.


title: Monadic encapsulation of effects: a revised approach (extended version)

authors:
Eugenio Moggi
Amr Sabry

abstract: Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the ad hoc type parameter of the original proposal. The second contribution is a type safety result for encapsulation of strict state using both the original encapsulation construct and the newly introduced one. We establish this result in a more expressive context than the original proposal, namely in the context of the higher-order lambda-calculus. The third contribution is a type safety result for encapsulation of lazy state in the higher-order lambda-calculus. This result resolves an outstanding open problem on which previous proof attempts failed. In all cases, we formalize the intended implementations as simple big-step operational semantics on untyped terms, which capture interesting implementation details not captured by the reduction semantics proposed previously.


title: Inductive benchmarking for purely functional data structures

authors:
Graeme E. Moss
Colin Runciman

abstract: Every designer of a new data structure wants to know how well it performs in comparison with others. But finding, coding and testing applications as benchmarks can be tedious and time-consuming. Besides, how a benchmark uses a data structure may considerably affect its apparent efficiency, so the choice of applications may bias the results. We address these problems by developing a tool for inductive benchmarking . This tool, Auburn , can generate benchmarks across a wide distribution of uses. We precisely define ‘the use of a data structure’, upon which we build the core algorithms of Auburn: how to generate a benchmark from a description of use, and how to extract a description of use from an application. We then apply inductive classification techniques to obtain decision trees for the choice between competing data structures. We test Auburn by benchmarking several implementations of three common data structures: queues, random-access lists and heaps. These and other results show Auburn to be a useful and accurate tool, but they also reveal some limitations of the approach.


title: How to look busy while being as lazy as ever: the implementation of a lazy functional debugger

abstract: This article describes the implementation of a debugger for lazy functional languages like Haskell. The key idea is to construct a declarative trace which hides the operational details of lazy evaluation. However, to avoid excessive memory consumption, the trace is constructed one piece at a time, as needed during a debugging session, by automatic re-execution of the program being debugged. The article gives a fairly detailed account of both the underlying ideas and of our implementation, and also presents performance figures which demonstrate the feasibility of the approach.


title: Modular lazy search for Constraint Satisfaction Problems

authors:
Thomas Nordin
Andrew P. Tolmach

abstract: We describe a unified, lazy, declarative framework for solving constraint satisfaction problems, an important subclass of combinatorial search problems. These problems are both practically significant and computationally hard. Finding solutions involves combining good general-purpose search algorithms with problem-specific heuristics. Conventional imperative algorithms are usually implemented and presented monolithically, which makes them hard to understand and reuse, even though new algorithms often are combinations of simpler ones. Lazy functional languages, such as Haskell, encourage modular structuring of search algorithms by separating the generation and testing of potential solutions into distinct functions communicating through an explicit, lazy intermediate data structure. But only relatively simple search algorithms have been treated this way in the past. Our framework uses a generic generation and pruning algorithm parameterized by a labeling function that annotates search trees with conflict sets. We show that many advanced imperative search algorithms, including conflict-directed backjumping, backmarking, minimal forward checking, and fail-first dynamic variable ordering, can be obtained by suitable instantiation of the labeling function. More importantly, arbitrary combinations of these algorithms can be built by simply composing their labeling functions. Our modular algorithms are as efficient as the monolithic imperative algorithms in the sense that they make the same number of consistency checks, and most of our algorithms are within a constant factor of their imperative counterparts in runtime and space usage. We believe our framework is especially well-suited for experimenting to find good combinations of algorithms for specific problems.


title: From Polyvariant flow information to intersection and union types

authors:
Jens Palsberg
Christina Pavlopoulou

abstract: Many polyvariant program analyses have been studied in the 1990s, including k -CFA, polymorphic splitting, and the cartesian product algorithm. The idea of polyvariance is to analyze functions more than once and thereby obtain better precision for each call site. In this paper we present an equivalence theorem which relates a co-inductively-defined family of polyvariant flow analyses and a standard type system. The proof embodies a way of understanding polyvariant flow information in terms of union and intersection types, and, conversely, a way of understanding union and intersection types in terms of polyvariant flow information. We use the theorem as basis for a new flow-type system in the spirit of the λ CIL -calculus of Wells, Dimock, Muller and Turbak, in which types are annotated with flow information. A flow-type system is useful as an interface between a flow-analysis algorithm and a program optimizer. Derived systematically via our equivalence theorem, our flow-type system should be a good interface to the family of polyvariant analyses that we study.


title: Set constraints for destructive array update optimization

authors:
Mitchell Wand
William D. Clinger

abstract: Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a multi-pass optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize and prove the soundness of these analyses using small-step operational semantics. We also prove that any sound liveness analysis induces a correct program transformation.


title: A predicative analysis of structural recursion

authors:
Andreas Abel
Thorsten Altenkirch

abstract: We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally, we point out how to do this proof predicatively using set based operators.


title: A calculus of module systems

authors:
Davide Ancona
Elena Zucca

abstract: We present CMS , a simple and powerful calculus of modules supporting mutual recursion and higher order features, which can be instantiated over an arbitrary core calculus satisfying standard assumptions. The calculus allows expression of a large variety of existing mechanisms for combining software components, including parameterized modules similar to ML functors, extension with overriding as in object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. Hence CMS can be used as a paradigmatic calculus for modular languages, in the same spirit the lambda calculus is used for functional programming. We first present an untyped version of the calculus and then a type system; we prove confluence, progress, and subject reduction properties. Then, we define a derived calculus of mixin modules directly in terms of CMS and show how to encode other primitive calculi into CMS (the lambda calculus and the Abadi-Cardelli object calculus). Finally, we consider the problem of introducing a subtype relation for module types.


title: Intensional polymorphism in type-erasure semantics

authors:
Karl Crary
Stephanie Weirich
J. Gregory Morrisett

abstract: Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling and attened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of run-time constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion. We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place, thereby avoiding certain beta-expansions required by other frameworks.


title: Region analysis and a pi-calculus with groups

authors:
Silvano Dal-Zilio
Andrew D. Gordon

abstract: We show that the typed region calculus of Tofte and Talpin can be encoded in a typed π-calculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and de-allocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our π-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the π-calculus with effects. We propose new equational laws for letregion , analogous to scope mobility laws in the π-calculus, and show them sound in our semantics.


title: Type-checking multi-parameter type classes

authors:
Dominic Duggan
John Ophel

abstract: Type classes are a novel combination of parametric polymorphism and constrained types. Although most implementations restrict type classes to be single-parameter, the generalization to multi-parameter type classes has gained increasing attention. A problem with multi-parameter type classes is the increased possibilities they introduce for ambiguity in inferred types, impacting their usefulness in many practical situations. A new type-checking strategy, domain-driven unifying resolution , is identified as an approach to solve these problems. Domain-driven unifying resolution is simple, efficient, and practically useful. However, even with severe restrictions on instance definitions, it is not possible to guarantee that type-checking with unifying resolution terminates. This is in contrast with the naive generalization of single parameter resolution strategies. Domain-driven unifying resolution is guaranteed to terminate if the type class constraints are satisfiable; however satisfiability is undecidable even with severe restrictions on instance definitions. These results shed some light on ambiguity problems with multi-parameter type classes.


title: A static semantics for Haskell

abstract: This paper gives a static semantics for Haskell 98, a non-strict purely functional programming language. The semantics formally specifies nearly all the details of the Haskell 98 type system, including the resolution of overloading, kind inference (including defaulting) and polymorphic recursion, the only major omission being a proper treatment of ambiguous overloading and its resolution. Overloading is translated into explicit dictionary passing, as in all current implementations of Haskell. The target language of this translation is a variant of the Girard–Reynolds polymorphic lambda calculus featuring higher order polymorphism and explicit type abstraction and application in the term language. Translated programs can thus still be type checked, although the implicit version of this system is impredicative. A surprising result of this formalization effort is that the monomorphism restriction, when rendered in a system of inference rules, compromises the principal type property.


title: DrScheme: a programming environment for Scheme

authors:
Robert Bruce Findler
John Clements
Cormac Flanagan
Matthew Flatt
Shriram Krishnamurthi
Paul Steckler
Matthias Felleisen

abstract: DrScheme is a programming environment for Scheme. It fully integrates a graphics-enriched editor, a parser for multiple variants of Scheme, a functional read-eval-print loop, and an algebraic printer. The environment is especially useful for students, because it has a tower of syntactically restricted variants of Scheme that are designed to catch typical student mistakes and explain them in terms the students understand. The environment is also useful for professional programmers, due to its sophisticated programming tools, such as the static debugger, and its advanced language features, such as units and mixins. Beyond the ordinary programming environment tools, DrScheme provides an algebraic stepper, a context-sensitive syntax checker, and a static debugger. The stepper reduces Scheme programs to values, according to the reduction semantics of Scheme. It is useful for explaining the semantics of linguistic facilities and for studying the behavior of small programs. The syntax checker annotates programs with font and color changes based on the syntactic structure of the program. On demand, it draws arrows that point from bound to binding occurrences of identifiers. It also supports α-renaming. Finally, the static debugger provides a type inference system that explains specific inferences in terms of a value-flow graph, selectively overlaid on the program text.


title: CPS in little pieces: composing partial continuations

authors:
Daniel P. Friedman
Amr Sabry

abstract: This paper presents a new two-stage CPS algorithm. The first stage plants trivial partial continuations via a recursive-descent traversal and the second stage is a rewrite system that transforms all nontail calls into tail calls. The algorithm combines the metaphors of the Plotkin-style CPS transformation along with reduction in the λ-calculus.


title: Recursive subtyping revealed

authors:
Vladimir Gapeyev
Michael Y. Levin
Benjamin C. Pierce

abstract: Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they relate to simpler declarative specifications is not widely understood, due in part to the difficulty of the available introductions to the area. This tutorial paper offers an ‘end-to-end’ introduction to recursive types and subtyping algorithms, from basic theory to efficient implementation, set in the unifying mathematical framework of coinduction.


title: A fresh look at binary search trees

abstract: Binary search trees are old hat, aren't they? Search trees are routinely covered in introductory computer science classes and they are widely used in functional programming courses to illustrate the benefits of algebraic data types and pattern matching. And indeed, the operation of insertion enjoys a succinct and elegant functional formulation. Figure 1 contains the six-liner given in the language Haskell 98. Alas, both succinctness and elegance are lost when it comes to implementing the dual operation of deletion, also shown in figure 1. Two additional helper functions are required causing the code size to double in comparison with insertion.


title: The countdown problem

abstract: We systematically develop a functional program that solves the countdown problem , a numbers game in which the aim is to construct arithmetic expressions satisfying certain constraints. Starting from a formal specification of the problem, we present a simple but inefficient program that solves the problem, and prove that this program is correct. We then use program fusion to calculate an equivalent but more efficient program, which is then further improved by exploiting arithmetic properties.


title: Secrets of the Glasgow Haskell Compiler inliner

authors:
Simon L. Peyton Jones
Simon Marlow

abstract: Higher-order languages such as Haskell encourage the programmer to build abstractions by composing functions. A good compiler must inline many of these calls to recover an efficiently executable program. In principle, inlining is dead simple: just replace the call of a function by an instance of its body. But any compiler-writer will tell you that inlining is a black art, full of delicate compromises that work together to give good performance without unnecessary code bloat. The purpose of this paper is, therefore, to articulate the key lessons we learned from a full-scale “production” inliner, the one used in the Glasgow Haskell compiler. We focus mainly on the algorithmic aspects, but we also provide some indicative measurements to substantiate the importance of various aspects of the inliner.


title: Developing a high-performance web server in Concurrent Haskell

abstract: Server applications, and in particular network-based server applications, place a unique combination of demands on a programming language: lightweight concurrency, high I/O throughput, and fault tolerance are all important. This paper describes a prototype web server written in Concurrent Haskell (with extensions), and presents two useful results: firstly, a conforming server could be written with minimal effort, leading to an implementation in less than 1500 lines of code, and secondly the naive implementation produced reasonable performance. Furthermore, making minor modifications to a few time-critical components improved performance to a level acceptable for anything but the most heavily loaded web servers.


title: Faking it: Simulating dependent types in Haskell

abstract: Dependent types reflect the fact that validity of data is often a relative notion by allowing prior data to affect the types of subsequent data. Not only does this make for a precise type system, but also a highly generic one: both the type and the program for each instance of a family of operations can be computed from the data which codes for that instance. Recent experimental extensions to the Haskell type class mechanism give us strong tools to relativize types to other types . We may simulate some aspects of dependent typing by making counterfeit type-level copies of data, with type constructors simulating data constructors and type classes simulating datatypes. This paper gives examples of the technique and discusses its potential.


title: Stack-based typed assembly language

authors:
J. Gregory Morrisett
Karl Crary
Neal Glew
David Walker

abstract: This paper presents STAL, a variant of Typed Assembly Language with constructs and types to support a limited form of stack allocation. As with other statically-typed low-level languages, the type system of STAL ensures that a wide class of errors cannot occur at run time, and therefore the language can be adapted for use in certifying compilers where security is a concern. Like the Java Virtual Machine Language (JVML), STAL supports stack allocation of local variables and procedure activation records, but unlike the JVML, STAL does not pre-suppose fixed notions of procedures, exceptions, or calling conventions. Rather, compiler writers can choose encodings for these high-level constructs using the more primitive RISC-like mechanisms of STAL. Consequently, some important optimizations that are impossible to perform within the JVML, such as tail call elimination or callee-saves registers, can be easily expressed within STAL.


title: The lambda calculus is algebraic

abstract: This paper serves as a self-contained, tutorial introduction to combinatory models of the untyped lambda calculus. We focus particularly on the interpretation of free variables. We argue that free variables should not be interpreted as elements in a model, as is usually done, but as indeterminates. We claim that the resulting interpretation is more natural and leads to a closer correspondence between models and theories. In particular, it solves the problem of the notorious ζ-rule, which asserts that equations should be preserved under binders, and which fails to be sound for the usual interpretation.


title: A typed representation for HTML and XML documents in Haskell

abstract: We define a family of embedded domain specific languages for generating HTML and XML documents. Each language is implemented as a combinator library in Haskell. The generated HTML/XML documents are guaranteed to be well-formed. In addition, each library can guarantee that the generated documents are valid XML documents to a certain extent (for HTML only a weaker guarantee is possible). On top of the libraries, Haskell serves as a meta language to define parameterized documents, to map structured documents to HTML/XML, to define conditional content, or to define entire web sites. The combinator libraries support element-transforming style , a programming style that allows programs to have a visual appearance similar to HTML/XML documents, without modifying the syntax of Haskell.


title: Parallel and Distributed Haskells

authors:
Philip W. Trinder
Hans-Wolfgang Loidl
Robert F. Pointon

abstract: Parallel and distributed languages specify computations on multiple processors and have a computation language to describe the algorithm, i.e. what to compute, and a coordination language to describe how to organise the computations across the processors. Haskell has been used as the computation language for a wide variety of parallel and distributed languages, and this paper is a comprehensive survey of implemented languages. We outline parallel and distributed language concepts and classify Haskell extensions using them. Similar example programs are used to illustrate and contrast the coordination languages, and the comparison is facilitated by the common computation language. A lazy language is not an obvious choice for parallel or distributed computation, and we address the question of why Haskell is a common functional computation language.


title: A calculus with polymorphic and polyvariant flow types

authors:
J. B. Wells
Allyn Dimock
Robert Muller
Franklyn A. Turbak

abstract: We present λ CIL , a typed λ-calculus which serves as the foundation for a typed intermediate language for optimizing compilers for higher-order polymorphic programming languages. The key innovation of λ CIL is a novel formulation of intersection and union types and flow labels on both terms and types. These flow types can encode polyvariant control and data flow information within a polymorphically typed program representation. Flow types can guide a compiler in generating customized data representations in a strongly typed setting. Since λ CIL enjoys confluence, standardization, and subject reduction properties, it is a valuable tool for reasoning about programs and program transformations.


title: "Trends in Functional Programming" (volumes 1 & 2) by Greg Michaelson, Phil Trinder and Hans-Wolfgang Loidl (editors volume 1), and Stephen Gilmore (editor volume 2). Intellect Books, Bristol, 2001, 2002

abstract: Trends in Functional Programming (volumes 1 & 2) by Greg Michaelson, Phil Trinder and Hans-Wolfgang Loidl (editors volume 1), and Stephen Gilmore (editor volume 2). Intellect Books, Bristol, 2001, 2002 - Volume 13 Issue 4


title: Setoids in type theory

authors:
Gilles Barthe
Venanzio Capretta
Olivier Pons

abstract: Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.


title: "Concepts in Programming Languages" by John C. Mitchell, Cambridge University Press, 2002, ISBN 0-521-78098-5


title: Closed types for a safe imperative MetaML

authors:
Cristiano Calcagno
Eugenio Moggi
Tim Sheard

abstract: This paper addresses the issue of safely combining computational effects and multi-stage programming. We propose a type system which exploits a notion of closed type , to check statically that an imperative multi-stage program does not cause run-time errors. Our approach is demonstrated formally for a core language called $\hbox{\sf MiniML}^{\sf meta}_{\sf ref}$ . This core language safely combines multi-stage constructs and ML-style references, and is a conservative extension of $\hbox{\sf MiniML}_{\sf ref}$ , a simple imperative subset of SML. In previous work, we introduced a closed type constructor , which was enough to ensure the safe execution of dynamically generated code in the pure fragment of $\hbox{\sf MiniML}^{\sf meta}_{\sf ref}$ .


title: Syntactic accidents in program analysis: on the impact of the CPS transformation

authors:
Daniel Damian
Olivier Danvy

abstract: We show that a non-duplicating transformation into Continuation-Passing Style (CPS) has no effect on control-flow analysis, a positive effect on binding-time analysis for traditional partial evaluation, and no effect on binding-time analysis for continuation-based partial evaluation: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, a monovariant binding-time analysis yields less precise results on a direct-style program than on its CPS counterpart, and an enhanced monovariant binding-time analysis yields equivalent results on a direct-style program and on its CPS counterpart. Our proof technique amounts to constructing the CPS counterpart of flow information and of binding times. Our results formalize and confirm a folklore theorem about traditional binding-time analysis, namely that CPS has a positive effect on binding times. What may be more surprising is that the benefit does not arise from a standard refinement of program analysis, as, for instance, duplicating continuations. The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.


title: CPS transformation of flow information, Part II: administrative reductions

abstract: We characterize the impact of a linear $\beta$ -reduction on the result of a control-flow analysis. (By ‘a linear $\beta$ -reduction’ we mean the $\beta$ -reduction of a linear $\lambda$ -abstraction, i.e., of a $\lambda$ -abstraction whose parameter occurs exactly once in its body.) As a corollary, we consider the administrative reductions of a Plotkin-style transformation into Continuation-Passing Style (CPS), and how they affect the result of a constraint-based control-flow analysis and, in particular, the least element in the space of solutions. We show that administrative reductions preserve the least solution. Preservation of least solutions solves a problem that was left open in Palsberg and Wand's article ‘CPS Transformation of Flow Information.’ Together, Palsberg and Wand's article and the present article show how to map in linear time the least solution of the flow constraints of a program into the least solution of the flow constraints of the CPS counterpart of this program, after administrative reductions. Furthermore, we show how to CPS transform control-flow information in one pass.


title: Compiling embedded languages

authors:
Conal Elliott
Sigbjørn Finne
Oege de Moor

abstract: Functional languages are particularly well-suited to the interpretive implementations of Domain-Specific Embedded Languages (DSELs). We describe an implemented technique for producing optimizing compilers for DSELs, based on Kamin's idea of DSELs for program generation. The technique uses a data type of syntax for basic types, a set of smart constructors that perform rewriting over those types, some code motion transformations, and a back-end code generator. Domain-specific optimization results from chains of domain-independent rewrites on basic types. New DSELs are defined directly in terms of the basic syntactic types, plus host language functions and tuples. This definition style makes compilers easy to write and, in fact, almost identical to the simplest embedded interpreters. We illustrate this technique with a language Pan for the computationally intensive domain of image synthesis and manipulation.


title: Welcome to the Educational Pearls Column

abstract: Education matters. The lack of education on functional programming languages and techniques is visible on a daily basis. Our students, co-workers, friends, and colleagues just don't know enough about these ideas and therefore often fail to implement the best possible solutions for their programming problems. The purpose of Educational Pearls is to address the education problem of our community from many different angles. It will include contributions on curricula issues, educational software support, and educational experiences. They will help teachers, professors, researchers, and software developers to promote functional programming languages and techniques in their respective contexts.


title: Verification of non-functional programs using interpretations in type theory

abstract: We study the problem of certifying programs combining imperative and functional features within the general framework of type theory. Type theory is a powerful specification language which is naturally suited for the proof of purely functional programs. To deal with imperative programs, we propose a logical interpretation of an annotated program as a partial proof of its specification. The construction of the corresponding partial proof term is based on a static analysis of the effects of the program which excludes aliases. The missing subterms in the partial proof term are seen as proof obligations, whose actual proofs are left to the user. We show that the validity of those proof obligations implies the total correctness of the program. This work has been implemented in the Coq proof assistant. It appears as a tactic taking an annotated program as argument and generating a set of proof obligations. Several nontrivial algorithms have been certified using this tactic.


title: Producing all ideals of a forest, functionally

authors:
Jean-Christophe Filliâtre
François Pottier

abstract: We present functional implementations of Koda and Ruskey's algorithm for generating all ideals of a forest poset as a Gray code. Using a continuation-based approach, we give an extremely concise formulation of the algorithm's core. Then, in a number of steps, we derive a first-order version whose efficiency is comparable to that of a C implementation given by Knuth.


title: Specification and correctness of lambda lifting

authors:
Adam Fischbach
John Hannan

abstract: We present a formal and general specification of lambda lifting and prove its correctness with respect to a call-by-name operational semantics. We use this specification to prove the correctness of a lambda lifting algorithm similar to the one proposed by Johnsson. Lambda lifting is a program transformation that eliminates free variables from functions by introducing additional formal parameters to function definitions and additional actual parameters to function calls. This operation supports the transformation from a lexically-structured functional program into a set of recursive equations. Existing results provide specific algorithms and only limited correctness results. Our work provides a more general specification of lambda lifting (and related operations) that supports flexible translation strategies, which may result in new implementation techniques. Our work also supports a simple framework in which the interaction of lambda lifting and other optimizations can be studied and from which new algorithms might be obtained.


title: AutoBayes: a system for generating data analysis programs from statistical models

authors:
Bernd Fischer
Johann Schumann

abstract: Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability theory and numerical analysis, are well-founded but difficult to implement: the development of a statistical data analysis program for any given application is time-consuming and requires substantial knowledge and experience in several areas. In this paper, we describe A UTO B AYES , a program synthesis system for the generation of data analysis programs from statistical models. A statistical model specifies the properties for each problem variable (i.e. observation or parameter) and its dependencies in the form of a probability distribution. It is a fully declarative problem description, similar in spirit to a set of differential equations. From such a model, A UTO B AYES generates optimized and fully commented C/C++ code which can be linked dynamically into the Matlab and Octave environments. Code is produced by a schema-guided deductive synthesis process. A schema consists of a code template and applicability constraints which are checked against the model during synthesis using theorem proving technology. A UTO B AYES augments schema-guided synthesis by symbolic-algebraic computation and can thus derive closed form solutions for many problems. It is well-suited for tasks like estimating best-fitting model parameters for the given data. Here, we describe A UTO B AYES 's system architecture, in particular the schema-guided synthesis kernel. Its capabilities are illustrated by a number of advanced textbook examples and benchmarks.


title: Programming graphical user interfaces with Scheme

authors:
Erick Gallesio
Manuel Serrano

abstract: This paper presents Biglook, a widget library for an extended version of the Scheme programming language. It uses classes of a Clos-like object layer to represent widgets and Scheme closures to handle graphical events. Combining functional and object-oriented programming styles yields an original application programming interface that advocates a strict separation between the implementation of the graphical interfaces and the user-associated commands, enabling compact source code. The Biglook implementation separates the Scheme programming interface and the native back-end. This permits different ports for Biglook. The current version uses GTK+ and Swing graphical toolkits, while the previous release used Tk.


title: "Implicit parallel programming in pH" by R. S. Nikhil and Arvind, Morgan Kaufmann, 2001

abstract: Having been out of academia for a number of years, I jumped at the chance to review these volumes, seeing this as an opportunity to get back up to speed with what was happening with the functional programming community.To give you some background, the point where I left to join industry was just after the world started using monads to structure their functional creations and I wondered what had come along since then.The two volumes actually draw together papers from the first two Scottish Functional Programming workshops.As such, the collected works read far more like conference proceedings, with each paper standing alone, than textbooks.However, the two volumes do succeed in bringing together papers under various headings:• parallel systems and programming, • type systems, • architectures and implementations, • applications, • theory,


title: Formatting: a class act

abstract: When I was a student, Simula was one of the languages taught in introductory programming language courses and I vividly remember a sticker one of our instructors had attached to the door of his office, saying “Simula does it with class”. I guess the same holds for Haskell except that Haskell replaces classes by type classes.


title: Regular expression pattern matching for XML

authors:
Haruo Hosoya
Benjamin C. Pierce

abstract: We propose regular expression pattern matching as a core feature of programming languages for manipulating XML. We extend conventional pattern-matching facilities (as in ML) with regular expression operators such as repetition (*) , alternation (|) , etc., that can match arbitrarily long sequences of subtrees, allowing a compact pattern to extract data from the middle of a complex sequence. We then show how to check standard notions of exhaustiveness and redundancy for these patterns. Regular expression patterns are intended to be used in languages with type systems based on regular expression types . To avoid excessive type annotations, we develop a type inference scheme that propagates type constraints to pattern variables from the type of input values. The type inference algorithm translates types and patterns into regular tree automata, and then works in terms of standard closure operations (union, intersection, and difference) on tree automata. The main technical challenge is dealing with the interaction of repetition and alternation patterns with the first-match policy, which gives rise to subtleties concerning both the termination and precision of the analysis. We address these issues by introducing a data structure representing these closure operations lazily.


title: Special issue on 'Logical frameworks and metalanguages'

abstract: There is both a great unity and a great diversity in presentations of logic. The diversity is staggering indeed – propositional logic, first-order logic, higher-order logic belong to one classification; linear logic, intuitionistic logic, classical logic, modal and temporal logics belong to another one. Logical deduction may be presented as a Hilbert style of combinators, as a natural deduction system, as sequent calculus, as proof nets of one variety or other, etc. Logic, originally a field of philosophy, turned into algebra with Boole, and more generally into meta-mathematics with Frege and Heyting. Professional logicians such as Gödel and later Tarski studied mathematical models, consistency and completeness, computability and complexity issues, set theory and foundations, etc. Logic became a very technical area of mathematical research in the last half century, with fine-grained analysis of expressiveness of subtheories of arithmetic or set theory, detailed analysis of well-foundedness through ordinal notations, logical complexity, etc. Meanwhile, computer modelling developed a need for concrete uses of logic, first for the design of computer circuits, then more widely for increasing the reliability of sofware through the use of formal specifications and proofs of correctness of computer programs. This gave rise to more exotic logics, such as dynamic logic, Hoare-style logic of axiomatic semantics, logics of partial values (such as Scott's denotational semantics and Plotkin's domain theory) or of partial terms (such as Feferman's free logic), etc. The first actual attempts at mechanisation of logical reasoning through the resolution principle (automated theorem proving) had been disappointing, but their shortcomings gave rise to a considerable body of research, developing detailed knowledge about equational reasoning through canonical simplification (rewriting theory) and proofs by induction (following Boyer and Moore successful integration of primitive recursive arithmetic within the LISP programming language). The special case of Horn clauses gave rise to a new paradigm of non-deterministic programming, called Logic Programming, developing later into Constraint Programming, blurring further the scope of logic. In order to study knowledge acquisition, researchers in artificial intelligence and computational linguistics studied exotic versions of modal logics such as Montague intentional logic, epistemic logic, dynamic logic or hybrid logic. Some others tried to capture common sense, and modeled the revision of beliefs with so-called non-monotonic logics. For the careful crafstmen of mathematical logic, this was the final outrage, and Girard gave his anathema to such “montres à moutardes”.


title: Short cut fusion is correct

abstract: Fusion is the process of removing intermediate data structures from modularly constructed functional programs. Short cut fusion is a particular fusion technique which uses a single, local transformation rule to fuse compositions of list-processing functions. Short cut fusion has traditionally been treated purely syntactically, and justifications for it have appealed either to intuition or to “free theorems” – even though the latter have not been known to hold in languages supporting higher-order polymorphic functions and fixpoint recursion. In this paper we use Pitts' recent demonstration that contextual equivalence in such languages is parametric to provide the first formal proof of the correctness of short cut fusion for them. In particular, we show that programs which have undergone short cut fusion are contextually equivalent to their unfused counterparts.


title: Haskell 98: Introduction

abstract: Contents i Preface vii 1.1 Program Structure 3 1.2 The Haskell Kernel 4 1.3 Values and Types 4 1.4 Namespaces 5


title: Haskell 98: Lexical Structure

abstract: 2.1 Notational Conventions 7 2.2 Lexical Program Structure 8 2.3 Comments 9 2.4 Identifiers and Operators 10 2.5 Numerical Literals 11 2.6 Character and String Literals 12 2.7 Layout 13


title: Haskell 98: Expressions

abstract: 3.1 Errors 19 3.2 Variables, Constructors, Operators, and Literals 20 3.3 Curried Applications and Lambda Abstractions 21 3.4 Operator Applications 21 3.5 Sections 22 3.6 Conditionals 23 3.7 Lists 23 3.8 Tuples 24 3.9 Unit Expressions and Parenthesized Expessions 25 3.10 Arithmetic Sequences 25 3.11 List Comprehensions 25 3.12 Let Expressions 27 3.13 Case Expressions 27 3.14 Do Expressions 29 3.15 Datatypes with Field Labels 29 3.16 Expression Type Signatures 32 3.17 Pattern Matching 32


title: Haskell 98: Declarations and Bindings

abstract: 4.1 Overview of Types and Classes 40 4.2 User-Defined datatypes 45 4.3 Type Classes and Overloading 49 4.4 Nested Declarations 55 4.5 Static Semantics of Function and Pattern Bindings 60 4.6 Kind Inference 66


title: Haskell 98: Modules

abstract: 5.1 Module Structure 68 5.2 Export Lists 69 5.3 Import Declarations 71 5.4 Importing and Exporting Instance Declarations 74 5.5 Name Clashes and Closure 74 5.6 Standard Prelude 77 5.7 Separate Compilation 78 5.8 Abstract Datatypes 78


title: Haskell 98: Predefined Types and Classes

abstract: 6.1 Standard Haskell Types 81 6.2 Strict Evaluation 84 6.3 Standard Haskell Classes 84 6.4 Numbers 91


title: Haskell 98: Basic Input/Output

abstract: 7.1 Standard I/O Functions 97 7.2 Sequencing I/O Operations 99 7.3 Exception Handling in the I/O Monad 100


title: Haskell 98: Standard Prelude

abstract: 8.1 Module Prelude 104 8.2 Module PreludeList 114 8.3 Module PreludeText 119 8.4 Module PreludeIO 123


title: Haskell 98: Syntax Reference

abstract: 9.1 Notational Conventions 125 9.2 Lexical Syntax 126 9.3 Layout 128 9.4 Literate Comments 131 9.5 Context-Free Syntax 133


title: Haskell 98: Specification of Derived Instances

abstract: 10.1 Derived Instances of Eq and Ord 140 10.2 Derived Instances of Enum 140 10.3 Derived Instances of Bounded 141 10.4 Derived Instances of Read and Show 142 10.5 An Example 143


title: Haskell 98: Compiler Pragmas

abstract: 11.1 Inlining 145 11.2 Specialization 145


title: Haskell 98 Libraries: Rational Numbers

abstract: 12.1 Library Ratio 150


title: Haskell 98 Libraries: Complex Numbers

abstract: 13.1 Library Complex 154


title: Haskell 98 Libraries: Numeric Functions

abstract: 14.1 Showing Functions 158 14.2 Reading Functions 159 14.3 Miscellaneous 159 14.4 Library Numeric 160


title: Haskell 98 Libraries: Indexing Operations

abstract: 15.1 Deriving Instances of Ix 170 15.2 Library Ix 171


title: Haskell 98 Libraries: Arrays

abstract: 16.1 Array Construction 174 16.2 Incremental Array Updates 175 16.3 Derived Arrays 176 16.4 Library Array 176


title: Haskell 98 Libraries: List Utilities

abstract: 17.1 Indexing Lists 181 17.2 “Set” Operations 181 17.3 List Transformations 182 17.4 unfoldr 182 17.5 Predicates 183 17.6 The “By” Operations 183 17.7 The “generic” Operations 184 17.8 Further “zip” Operations 184 17.9 Library List 184


title: Haskell 98 Libraries: Maybe Utilities

abstract: 18.1 Library Maybe 192


title: Haskell 98 Libraries: Character Utilities

abstract: 19.1 Library Char 195


title: Haskell 98 Libraries: Monad Utilities

abstract: 20.1 Naming Conventions 200 20.2 Class MonadPlus 200 20.3 Functions 201 20.4 Library Monad 202


title: Haskell 98 Libraries: Input/Output

abstract: 21.1 I/O Errors 207 21.2 Files and Handles 208 21.3 Opening and Closing Files 210 21.4 Determining the Size of a File 211 21.5 Detecting the End of Input 211 21.6 Buffering Operations 211 21.7 Repositioning Handles 213 21.8 Handle Properties 213 21.9 Text Input and Output 214 21.10 Examples 215 21.11 Library IO 216


title: Haskell 98 Libraries: Directory Functions

abstract: Directory Functions 219


title: Haskell 98 Libraries: System Functions

abstract: System Functions 223


title: Haskell 98 Libraries: Dates and Times

abstract: 24.1 Library Time 227


title: Haskell 98 Libraries: Locales

abstract: 25.1 Library Locale 231


title: Haskell 98 Libraries: CPU Time

abstract: CPU Time 233


title: Haskell 98 Libraries: Random Numbers

abstract: 27.1 The RandomGen class, and the StdGen generator 236 27.2 The Random class 239 27.3 The global random number generator 240


title: Haskell 98 Libraries: Bibliography

abstract: Bibliography 241 Index 243


title: The Educational Pearls column

authors:
Simon L. Peyton Jones
Philip Wadler


title: "Structure and Interpretation of Classical Mechanics" by Gerald Jay Sussman and Jack Wisdom with Meinhard E. Mayer, The MIT Press; 2001, ISBN 0262194554

abstract: Having been out of academia for a number of years, I jumped at the chance to review these volumes, seeing this as an opportunity to get back up to speed with what was happening with the functional programming community.To give you some background, the point where I left to join industry was just after the world started using monads to structure their functional creations and I wondered what had come along since then.The two volumes actually draw together papers from the first two Scottish Functional Programming workshops.As such, the collected works read far more like conference proceedings, with each paper standing alone, than textbooks.However, the two volumes do succeed in bringing together papers under various headings:• parallel systems and programming, • type systems, • architectures and implementations, • applications, • theory,


title: "The World of Scripting Languages" by David W. Barron, John Wiley & Sons, 2000, ISBN 0-471-99886-9

abstract: Having been out of academia for a number of years, I jumped at the chance to review these volumes, seeing this as an opportunity to get back up to speed with what was happening with the functional programming community.To give you some background, the point where I left to join industry was just after the world started using monads to structure their functional creations and I wondered what had come along since then.The two volumes actually draw together papers from the first two Scottish Functional Programming workshops.As such, the collected works read far more like conference proceedings, with each paper standing alone, than textbooks.However, the two volumes do succeed in bringing together papers under various headings:


title: TinkerType: a language for playing with formal systems

authors:
Michael Y. Levin
Benjamin C. Pierce

abstract: TinkerType is a pragmatic framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses – individual inference rules – and a set of features controlling the inclusion of clauses in particular systems. Simple static checks are used to help maintain consistency of the generated systems. We present TinkerType and its implementation and describe its application to two substantial repositories of typed lambda-calculi. The first repository covers a broad range of typing features, including subtyping, polymorphism, type operators and kinding, computational effects, and dependent types. It describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler , to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers. The second repository addresses a smaller collection of systems, and provides modularized proofs of basic safety properties.


title: PAL+: a lambda-free logical framework

abstract: A lambda-free logical framework takes parameterisation and definitions as the basic notions to provide schematic mechanisms for specification of type theories and their use in practice. The framework presented here, PAL + , is a logical framework for specification and implementation of type theories, such as Martin-Löf's type theory or UTT. As in Martin-Löf's logical framework (Nordström et al. , 1990), computational rules can be introduced and are used to give meanings to the declared constants. However, PAL + only allows one to talk about the concepts that are intuitively in the object type theories: types and their objects, and families of types and families of objects of types. In particular, in PAL + , one cannot directly represent families of families of entities, which could be done in other logical frameworks by means of lambda abstraction. PAL + is in the spirit of de Bruijn's PAL + for Automath (de Bruijn, 1980). Compared with PAL, PAL + allows one to represent parametric concepts such as families of types and families of non-parametric objects, which can be used by themselves as totalities as well as when they are fully instantiated. Such parametric objects are represented by local definitions (let-expressions). We claim that PAL + is a correct meta-language for specifying type theories (e.g., dependent type theories), as it has the advantage of exactly capturing the intuitive concepts in object type theories, and that its implementation reflects the actual use of type theories in practice. We shall study the meta-theory of PAL + by developing its typed operational semantics and showing that it has nice meta-theoretic properties.


title: Haskell in Space

abstract: This paper describes a practical exercise set to an introductory functional programming course. The exercise is to implement a small game involving a space ship in an asteroids belt, after the fashion of the classic Asteroids arcade game. The positive experience suggests that interactive graphics programs of this kind make good and entertaining programming exercises for functional programming courses.


title: First-order unification by structural recursion

abstract: First-order unification algorithms (Robinson, 1965) are traditionally implemented via general recursion, with separate proofs for partial correctness and termination. The latter tends to involve counting the number of unsolved variables and showing that this total decreases each time a substitution enlarges the terms. There are many such proofs in the literature (Manna & Waldinger, 1981; Paulson, 1985; Coen, 1992; Rouyer, 1992; Jaume, 1997; Bove, 1999). This paper shows how a dependent type can relate terms to the set of variables over which they are constructed. As a consequence, first-order unification becomes a structurally recursive program, and a termination proof is no longer required. Both the program and its correctness proof have been checked using the proof assistant L EGO (Luo & Pollack, 1992; McBride, 1999).


title: Inlining as staged computation

authors:
Stefan Monnier
Zhong Shao

abstract: Inlining and specialization appear in various forms throughout the implementation of modern programming languages. From mere compiler optimizations to sophisticated techniques in partial evaluation, they are omnipresent, yet each application is treated differently. This paper is an attempt at uncovering the relations between inlining (as done in production compilers) and staged computation (as done in partial evaluators) in the hope of bringing together the research advances in both fields. Using a two-level lambda calculus as the intermediate language, we show how to model inlining as a staged computation while avoiding unnecessary code duplication. The new framework allows us to define inlining annotations formally and to reason about their interactions with module code. In fact, we present a cross-module inlining algorithm that inlines all functions marked inlinable, even in the presence of ML-style parameterized modules.


title: Stack-based typed assembly language

abstract: The following three figures (figures 10, 11 and 12) were not shown in the original published version of the article. These figures constitute the entire static semantics of the STAL type system.


title: On bunched typing

abstract: We study a typing scheme derived from a semantic situation where a single category possesses several closed structures, corresponding to different varieties of function type. In this scheme typing contexts are trees built from two (or more) binary combining operations, or in short, bunches . Bunched typing and its logical counterpart, bunched implications, have arisen in joint work of the author and David Pym. The present paper gives a basic account of the type system, and then focusses on concrete models that illustrate how it may be understood in terms of resource access and sharing. The most basic system has two context-combining operations, and the structural rules of Weakening and Contraction are allowed for one but not the other. This system includes a multiplicative, or substructural, function type −∗ alongside the usual (additive) function type $\rightarrow$ ; it is dubbed the $\alpha\lambda$ -calculus after its binders, $\alpha$ for the $\alpha$ dditive binder and $\lambda$ for the multiplicative, or $\lambda$ inear, binder. We show that the features of this system are, in a sense, complementary to calculi based on linear logic; it is incompatible with an interpretation where a multiplicative function uses its argument once, but perfectly compatible with a reading based on sharing of resources. This sharing interpretation is derived from syntactic control of interference, a type-theoretic method of controlling sharing of storage, and we show how bunch-based management of Contraction can be used to provide a more flexible type system for interference control.


title: Theoretical Pearls

abstract: A combinator expression is flat if it can be written without parentheses, that is, if all applications nest to the left, never to the right. This note explores a simple method for flattening combinator expressions involving arbitrary combinators.


title: CPS transformation of flow information

authors:
Jens Palsberg
Mitchell Wand

abstract: We consider the question of how a Continuation-Passing-Style (CPS) transformation changes the flow analysis of a program. We present an algorithm that takes the least solution to the flow constraints of a program and constructs in linear time the least solution to the flow constraints for the CPS-transformed program. Previous studies of this question used CPS transformations that had the effect of duplicating code, or of introducing flow sensitivity into the analysis. Our algorithm has the property that for a program point in the original program and the corresponding program point in the CPS-transformed program, the flow information is the same. By carefully avoiding both duplicated code and flow-sensitive analysis, we find that the most accurate analysis of the CPS-transformed program is neither better nor worse than the most accurate analysis of the original. Thus a compiler that needed flow information after CPS transformation could use the flow information from the original program to annotate some program points, and it could use our algorithm to find the rest of the flow information quickly, rather than having to analyze the CPS-transformed program.


title: Pragmatic aspects of reusable program generators

abstract: When writing a program generator requires considerable intellectual effort, it is valuable to amortize that effort by using the generator to build more than one application. When a program generator serves multiple clients, however, the implementor must address pragmatic questions that implementors of single-use program generators can ignore. In how many languages should generated code be written? How should code be packaged? What should the interfaces to the client code look like? How should a user control variations? This paper elaborates on these questions by means of case studies of the New Jersey Machine-Code Toolkit, the $\lambda$ -RTL Translator, and the ASDL program generator. It is hoped that the paper will stimulate the development of better techniques. Most urgently needed are a standard way to support multiple target languages and a simple, clear way to control interfaces to generated code.


title: A fully adequate shallow embedding of the [pi]-calculus in Isabelle/HOL with mechanized syntax analysis

authors:
Christine Röckl
Daniel Hirschkoff

abstract: This paper discusses an application of the higher-order abstract syntax technique to general-purpose theorem proving, yielding shallow embeddings of the binders of formalized languages. Higher-order abstract syntax has been applied with success in specialized logical frameworks which satisfy a closed-world assumption. As more general environments (like Isabelle/HOL or Coq) do not support this closed-world assumption, higher-order abstract syntax may yield exotic terms, that is, datatypes may produce more terms than there should actually be in the language. The work at hand demonstrates how such exotic terms can be eliminated by means of a two-level well-formedness predicate, further preparing the ground for an implementation of structural induction in terms of rule induction, and hence providing fully-fledged syntax analysis. In order to apply and justify well-formedness predicates, the paper develops a proof technique based on a combination of instantiations and reabstractions of higher-order terms. As an application, syntactic principles like the theory of contexts (as introduced by Honsell, Miculan, and Scagnetto) are derived, and adequacy of the predicates is shown, both within a formalization of the π-calculus in Isabelle/HOL.


title: "Algorithms: A Functional Programming Approach" by Fethi Rabhi and Guy Lapalme, Addison-Wesley, 1999, ISBN 0-201-59604-0, xi + 235pp


title: Single Assignment C: efficient support for high-level array operations in a functional setting

abstract: This paper presents a novel approach for integrating arrays with access time ${\cal O}$(1) into functional languages. It introduces n-dimensional arrays combined with a type system that supports hierarchies of array types with varying shape information as well as a shape-invariant form of array comprehension called WITH -loop. Together, these constructs allow for a programming style similar to that of array programming languages such as A PL . We use Single Assignment C (S A C), a functional C-variant aimed at numerical applications that is based on the proposed design, to demonstrate that programs written in that style can be compiled to code whose runtime performance is competitive with that of hand-optimized Fortran programs. However, essential prerequisites for such performance figures are a shape inference system integrated in the type system as well as several high-level optimizations. Most notably of these is With Loop Folding , an optimization technique for eliminating intermediate arrays.


title: Compiling for template-based run-time code generation

authors:
Frederick Smith
Dan Grossman
J. Gregory Morrisett
Luke Hornof
Trevor Jim

abstract: Cyclone is a type-safe programming language that provides explicit run-time code generation. The Cyclone compiler uses a template-based strategy for run-time code generation in which pre-compiled code fragments are stitched together at run time. This strategy keeps the cost of code generation low, but it requires that optimizations, such as register allocation and code motion, are applied to templates at compile time. This paper describes a principled approach to implementing such optimizations. In particular, we generalize standard flow-graph intermediate representations to support templates, define a mapping from (a subset of) Cyclone to this representation, and describe a dataflow-analysis framework that supports standard optimizations across template boundaries.


title: Semantics, Applications, and Implementation of Program Generation

abstract: This special issue of the Journal of Functional Programming follows up on the First International ACM SIGPLAN Workshop on the Semantics, Applications, and Implementation of Program Generators (SAIG 2000). The special issue contains eight full length papers, which were received based on an open call for papers. Six of these papers are substantially extended revisions of papers presented at the workshop itself.


title: "Essentials of Programming Languages" (2nd ed) by Daniel P. Friedman, Mitchell Wand and Christopher T. Haynes, MIT Press, ISBN 0-262-06217-8, 2001


title: Program specialization for execution monitoring

abstract: Execution monitoring is a proven tool for securing program execution and to enforce safety properties on applets and mobile code, in particular. Inlining monitoring tools perform their task by inserting certain run-time checks into the monitored application before executing it. For efficiency reasons, they attempt to insert as few checks as possible using techniques ranging from simple ad hoc optimizations to theorem proving. Partial evaluation is a powerful tool for specifying and implementing program transformations. The present work demonstrates that standard partial evaluation techniques are sufficient to transform an interpreter equipped with monitoring code into a non-standard compiler. This compiler generates application code, which contains the inlined monitoring code. If the monitor is enforcing a security policy, then the result is a secured application code. If the policy is defined using a security automaton, then the transformation can elide many run-time checks by using abstract interpretation. Our approach relies on proper staging of the monitoring interpreter. The transformation runs in linear time, produces code linear in the size of the original program, and is guaranteed not to duplicate incoming code.


title: Termination of rewriting in the Calculus of Constructions

abstract: We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewriting rules over dependently typed function symbols. We prove strong normalization for any term rewriting system, such that all function symbols satisfy the, so called, star dependency condition, and every rule is accepted by the Higher Order Recursive Path Ordering (which is an extension of the method created by Jouannaud and Rubio for the setting of the simply typed lambda calculus). The proof of strong normalization is done by using a typed version of reducibility candidates due to Coquand and Gallier. Our criterion is general enough to accept definitions by rewriting of many well-known higher order functions, for example dependent recursors for inductive types or proof carrying functions. This makes it a very good candidate for inclusion in a proof assistant based on the Curry-Howard isomorphism.


title: Concurrent distinct choices

authors:
Sergio Antoy
Michael Hanus

abstract: An injective finite mapping is an abstraction common to many programs. We describe the design of an injective finite mapping and its implementation in Curry, a functional logic language. Curry supports the concurrent asynchronous execution of distinct portions of a program. This condition prevents passing from one portion to another a structure containing a partially constructed mapping to ensure that a new choice does not violate the injectivity condition. We present some motivating problems and we show fragments of programs that solve these problems using our design and implementation.


title: Dependent types ensure partial correctness of theorem provers

authors:
Andrew W. Appel
Amy P. Felty

abstract: Static type systems in programming languages allow many errors to be detected at compile time that wouldn't be detected until runtime otherwise. Dependent types are more expressive than the type systems in most programming languages, so languages that have them should allow programmers to detect more errors earlier. In this paper, using the Twelf system, we show that dependent types in the logic programming setting can be used to ensure partial correctness of programs which implement theorem provers, and thus avoid runtime errors in proof search and proof construction. We present two examples: a tactic-style interactive theorem prover and a union-find decision procedure.


title: Parsing permutation phrases

authors:
Arthur I. Baars
Andres Löh
S. Doaitse Swierstra

abstract: A permutation phrase is a sequence of elements (possibly of different types) in which each element occurs exactly once and the order is irrelevant. Some of the permutable elements may be optional. We show how to extend a parser combinator library with support for parsing such free-order constructs. A user of the library can easily write parsers for permutation phrases and does not need to care about checking and reordering the recognized elements. Applications include the generation of parsers for attributes of XML tags and Haskell's record syntax.


title: Constructed product result analysis for Haskell

authors:
Clement A. Baker-Finch
Kevin Glynn
Simon L. Peyton Jones

abstract: Compilers for ML and Haskell typically go to a good deal of trouble to arrange that multiple arguments can be passed efficiently to a procedure. For some reason, less effort seems to be invested in ensuring that multiple results can also be returned efficiently. In the context of the lazy functional language Haskell, we describe an analysis, Constructed Product Result (CPR) analysis, that determines when a function can profitably return multiple results in registers. The analysis is based only on a function's definition, and not on its uses (so separate compilation is easily supported) and the results of the analysis can be expressed by a transformation of the function definition alone. We discuss a variety of design issues that were addressed in our implementation, and give measurements of the effectiveness of our approach across a substantial benchmark set. Overall, the price/performance ratio is good: the benefits are modest in general (though occasionally dramatic), but the costs in both complexity and compile time, are low.


title: Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming

authors:
Gilles Barthe
Peter Dybjer
Peter Thiemann

abstract: Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.


title: On tiling a chessboard

abstract: Teacher: Good morning class. Today I would like you to construct a program for finding out how many ways a chessboard can be tiled with dominoes. For those who don't play games, a chessboard is a 8×8 board divided into 64 squares, and a domino is a 2×1 tile which can cover two squares of the board either vertically or horizontally. For example, a 2×2 board can be covered with two dominoes in exactly two ways, with both dominoes horizontal or both vertical.


title: Inverting the Burrows-Wheeler transform

authors:
Richard S. Bird
Shin-Cheng Mu

abstract: The Burrows–Wheeler Transform is a string-to-string transform which, when used as a preprocessing phase in compression, significantly enhances the compression rate. However, it often puzzles people how the inverse transform is carried out. In this pearl we to exploit simple equational reasoning to derive the inverse of the Burrows–Wheeler transform from its specification. We also outline how to derive the inverse of two more general versions of the transform, one proposed by Schindler and the other by Chapin and Tate.


title: The recursive record semantics of objects revisited

abstract: In a call-by-value language, representing objects as recursive records requires using an unsafe fixpoint. We design, for a core language including extensible records, a type system which rules out unsafe recursion and still supports the construction of a principal type for each typable term. We illustrate the expressive power of this language with respect to object-oriented programming by introducing a sub-language for “mixin-based” programming.


title: The risks and benefits of teaching purely functional programming in first year

authors:
Manuel M. T. Chakravarty
Gabriele Keller

abstract: We argue that teaching purely functional programming as such in freshman courses is detrimental to both the curriculum as well as to promoting the paradigm. Instead, we need to focus on the more general aims of teaching elementary techniques of programming and essential concepts of computing. We support this viewpoint with experience gained during several semesters of teaching large first-year classes (up to 600 students) in Haskell. These classes consisted of computer science students as well as students from other disciplines. We have systematically gathered student feedback by conducting surveys after each semester. This article contributes an approach to the use of modern functional languages in first year courses and, based on this, advocates the use of functional languages in this setting.


title: Parallel Parsing Processes

abstract: We derive a combinator library for non-deterministic parsers with a monadic interface, by means of successive refinements starting from a specification. The choice operator of the parser implements a breadth-first search rather than the more common depth-first search, and can be seen as a parallel composition between two parsing processes. The resulting library is simple and efficient for “almost deterministic” grammars, which are typical for programming languages and other computing science applications.


title: Programming Methodology A. McIver and C. Morgan, editors, Springer-Verlag, 2002

abstract: This book describes theoretical results about AnsProlog * that have been obtained over the past decade.AnsProlog * or Prolog with Answer Sets 1 is a variation of the Prolog programming language, and extends the language by allowing clauses of the form:in the program.The L i 's are the literals (or atoms) of the Prolog language and may be supplied with a prefix ¬ sign, indicating the negation of a literal, while the prefix of not indicates negation as failure.Hence the semantics of the clause (C) may be read as follows: if all the literals L1, . . ., L m are true and all the literals L m+1 , . . ., L n can be safely assumed false then at least one of the literals L 1 , . . ., L k is true.(The actual semantics of each AnsProlog * program will be defined in terms of the Herbrand Universe of ground terms and the Herbrand Base of ground atoms.)The book takes the approach that the clause (C) is the most general form of a clause in the AnsProlog * language and so various subclasses of AnsProlog * can be defined by restricting this clause.For example: an AnsProlog -not program is when none of the clauses of a program contain the prefix not.In this respect, the book discusses the tractability, the complexity, the expressibility of the various subclasses of AnsProlog * based on the premise that AnsProlog * is both an excellent knowledge representation language and that it has a number of advantages over the Prolog language implementations based on SLDNF.For example, the ordering of goals within a clause and the ordering of clauses within a Prolog program affects whether a solution can or cannot be found (i.e. the program might get into an infinite loop); but not this is not the case within an AnsProlog * program.The reason being is that the semantics of an implementation of the AnsProlog * language can be thought of as allowing all models of the program to exist and then by using the clauses within the program, to impose restrictions on these models.The actual model(s) produced can then be interpreted in either a bi-valent (where a ground atom is either true or false) fashion or a tri-valent (where a ground atom is either true, false or unknown) fashion.The implementation algorithms describing how to restrict the models are described in Chapter 7 and two systems implementing the AnsProlog * language (and various subclasses), viz: (i) lparse+smodels and (ii) dlv are discussed in Chapter 8.The lparse+smodels program produces the stable models (or bi-valent) implementation, while the dlv produces the well-founded models (or tri-valent) implementation.Baral does note that both systems are under development and so implying that Chapter 8 may be out of date within a few years.However this aspect is compensated by Baral having a website www.baral.us/bookonewhere hypertext links to both the two systems and an errata/additional notes for the book are presented.On the application side, the book is peppered with many examples and simple programs illustrating the current point being made in the text.For example: how various forms of the 1 AnsProlog * is sometimes called A-Prolog in the literature.


title: Escape from Zurg: an exercise in logic programming

abstract: In this Pearl we illustrate with an example that modern functional programming languages like Haskell can be used effectively for programming search problems, in contrast to the widespread belief that Prolog is much better suited for tasks like these.


title: The structure and interpretation of the computer science curriculum

authors:
Matthias Felleisen
Robert Bruce Findler
Matthew Flatt
Shriram Krishnamurthi

abstract: Twenty years ago Abelson and Sussman's Structure and Interpretation of Computer Programs radically changed the intellectual landscape of introductory computing courses. Instead of teaching some currently fashionable programming language, it employed Scheme and functional programming to teach important ideas. Introductory courses based on the book showed up around the world and made Scheme and functional programming popular. Unfortunately, these courses quickly disappeared again due to shortcomings of the book and the whimsies of Scheme. Worse, the experiment left people with a bad impression of Scheme and functional programming in general. In this pearl, we propose an alternative role for functional programming in the first-year curriculum. Specifically, we present a framework for discussing the first-year curriculum and, based on it, the design rationale for our book and course, dubbed How to Design Programs . The approach emphasizes the systematic design of programs. Experience shows that it works extremely well as a preparation for a course on object-oriented programming.


title: Linearization of the lambda-calculus and its relation with intersection type systems

authors:
Mário Florido
Luís Damas

abstract: In this paper we present a notion of expansion of a term in the lambda-calculus which transforms terms into linear terms. This transformation replaces each occurrence of a variable in the original term by a fresh variable taking into account non-trivial implications in the structure of the term caused by these simple replacements. We prove that the class of terms which can be expanded is the same of terms typable in an Intersection Type System, i.e. the strongly normalizable terms. We then show that expansion is preserved by weak-head reduction, the reduction considered by functional programming languages.


title: Transformation techniques for context-sensitive rewrite systems

authors:
Jürgen Giesl
Aart Middeldorp

abstract: Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyze the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too. We analyze the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensitive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity.


title: The Fun of Programming edited by Jeremy Gibbons and Oege de Moor, Palgrave Macmillan, 2003


title: The Functional "C" experience

authors:
Pieter H. Hartel
Henk L. Muller
Hugh Glaser

abstract: A functional programming language can be taught successfully as a first language, but if there is no follow up the students do not appreciate the functional approach. Following discussions concerning this issue at the 1995 FPLE conference (Hartel & Plasmeijer, 1995), we decided to develop such a follow up by writing a book that teaches C to students who can write simple functional programs. This paper summarises the essence of our approach, which is based on program transformation, and presents our experience teaching functional C at the Universities of Southampton and Bristol.


title: Computer literacy via Scheme and web programming

abstract: We describe an approach to introducing non-science majors to programming and computation in part by teaching them applets, servlets, and groupware applications. The course uses a dialect of didactic Scheme that is implemented in, and tightly integrated with, Java. The declarative nature of our approach allows non-science majors with no programming background to develop surprisingly complex web applications in about half a semester. This level of programming provides a context for a deeper understanding of computation than is usually feasible in a Computer Literacy course.


title: Special issue on functional pearls Editorial

abstract: You are holding a necklace in your hands, composed of no fewer than thirteen exquisite pearls. The pearls are from all over the world, selected for the finest quality, smoothness and lustre. For your viewing pleasure, the necklace emphasizes variety, stringing pearls of wildly different color, shape and size. Satisfaction is guaranteed.


title: Editorial

authors:
Paul Hudak
Greg Morrisett

abstract: This issue of the Journal of Functional Programming marks a point of transition. Our long-time Chief Editors, Simon Peyton Jones and Philip Wadler, are stepping down. Most of us are aware of the amazing research contributions that Simon and Phil have made to functional programming. But you may not be aware how much these two have put in behind the scenes.


title: Global variables in Haskell

abstract: Haskell today provides good support not only for a functional programming style, but also for an imperative one. Elements of imperative programming are needed in applications such as web servers, or to provide efficient implementations of well-known algorithms, such as many graph algorithms. However, one element of imperative programming, the global variable , is surprisingly hard to emulate in Haskell. We discuss several existing methods, none of which is really satisfactory, and finally propose a new approach based on implicit parameters. This approach is simple, safe, and efficient, although it does reveal weaknesses in Haskell's present type system.


title: Composing fractals

abstract: This paper describes a simple but flexible family of Haskell programs for drawing pictures of fractals such as Mandelbrot and Julia sets. Its main goal is to showcase the elegance of a compositional approach to program construction, and the benefits of a clean separation between different aspects of program behavior. Aimed at readers with relatively little experience of functional programming, the paper can be used as a tutorial on functional programming, as an overview of the Mandelbrot set, or as a motivating example for studies in computability.


title: Pickler combinators

abstract: The tedium of writing pickling and unpickling functions by hand is relieved using a combinator library similar in spirit to the well-known parser combinators. Picklers for primitive types are combined to support tupling, alternation, recursion, and structure sharing. Code is presented in Haskell; an alternative implementation in ML is discussed.


title: Building reliable, high-performance networks with the Nuprl proof development system

abstract: Proof systems for expressive type theories provide a foundation for the verification and synthesis of programs. But despite their successful application to numerous programming problems there remains an issue with scalability. Are proof environments capable of reasoning about large software systems? Can the support they offer be useful in practice? In this article we answer this question by showing how the N UPRL proof development system and its rich type theory have contributed to the design of reliable, high-performance networks by synthesizing optimized code for application configurations of the E NSEMBLE group communication toolkit. We present a type-theoretical semantics of OC AML , the implementation language of E NSEMBLE , and tools for automatically importing system code into the N UPRL system. We describe reasoning strategies for generating verifiably correct fast-path optimizations of application configurations that substantially reduce end-to-end latency in E NSEMBLE . We also discuss briefly how to use N UPRL for checking configurations against specifications and for the design of reliable adaptive network protocols.


title: Functional chart parsing of context-free grammars

abstract: This paper implements a simple and elegant version of bottom-up Kilbury chart parsing (Kilbury, 1985; Wirén, 1992). This is one of the many chart parsing variants, which are all based on the data structure of charts. The chart parsing process uses inference rules to add new edges to the chart, and parsing is complete when no further edges can be added. One novel aspect of this implementation is that it doesn't have to rely on a global state for the implementation of the chart. This makes the code clean, elegant and declarative, while still having the same space and time complexity as the standard imperative implementations.


title: Développement d'applications avec Objective CAML by E. Chailloux, P. Manoury and B. Pagano, O'Reilley, 2003


title: Linear lambda calculus and PTIME-completeness

abstract: We give transparent proofs of the PTIME-completeness of two decision problems for terms in the λ-calculus. The first is a reproof of the theorem that type inference for the simply-typed λ-calculus is PTIME-complete. Our proof is interesting because it uses no more than the standard combinators Church knew of some 70 years ago, in which the terms are linear affine – each bound variable occurs at most once. We then derive a modification of Church's coding of Booleans that is linear, where each bound variable occurs exactly once. A consequence of this construction is that any interpreter for linear λ-calculus requires polynomial time. The logical interpretation of this consequence is that the problem of normalizing proofnets for multiplicative linear logic (MLL) is also PTIME-complete.


title: Functional satisfaction

abstract: This work presents simple decision procedures for the propositional calculus and for a simple predicate calculus. These decision procedures are based upon enumeration of the possible values of the variables in an expression. Yet, by taking advantage of the sequential semantics of boolean connectors, not all values are enumerated. In some cases, dramatic savings of machine time can be achieved. In particular, an equivalence checker for a small programming language appears to be usable in practice.


title: The view from the left

authors:
Conor McBride
James McKinna

abstract: Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type $\mathit{T}$ , and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem , one which establishes the validity of a new induction principle for $\mathit{T}$ . We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.


title: Enumerating the strings of regular languages

abstract: Haskell code is developed for two ways to list the strings of the language defined by a regular expression: directly by set operations and indirectly by converting to and simulating an equivalent automaton. The exercise illustrates techniques for dealing with infinite ordered domains and leads to an effective standard form for nondeterministic finite automata.


title: Functional programming with the FC++ library

authors:
Brian McNamara
Yannis Smaragdakis

abstract: We describe the FC++ library, a rich library supporting functional programming in C++. Prior approaches to encoding higher order functions in C++ have suffered with respect to polymorphic functions from either lack of expressiveness or high complexity. In contrast, FC++ offers full and concise support for higher-order polymorphic functions through a novel use of C++ type inference. The FC++ library has a number of useful features, including a generalized mechanism to implement currying in C++, a “lazy list” class which enables the creation of “infinite data structures”, a subtype polymorphism facility, and an extensive library of useful functions, including a large part of the Haskell Standard Prelude. The FC++ library has an efficient implementation. We show the results of a number of experiments which demonstrate the value of optimizations we have implemented. These optimizations have improved the run-time performance by about an order of magnitude for some benchmark programs that make heavy use of FC++ lazy lists. We also make an informal performance comparison with similar programs written in Haskell.


title: Calculating the Sieve of Eratosthenes

abstract: The Sieve of Eratosthenes is an efficient algorithm for computing the successive primes. Rendered informally, it is as follows: 1. Write down the successive “plurals”: 2, 3, 4, … 2. Repeat: (a) Take the first number that is not circled or crossed out. (b) Circle it. (c) Cross out its proper multiples. 3. What is left (i.e. the circled numbers) are the successive prime numbers.


title: Derivation of a logarithmic time carry lookahead addition circuit

authors:
John T. O'Donnell
Gudula Rünger

abstract: Using Haskell as a digital circuit description language, we transform a ripple carry adder that requires $O(n)$ time to add two $n$ -bit words into a parallel carry lookahead adder that requires $O(\log n)$ time. The ripple carry adder uses a scan function to calculate carry bits, but this scan cannot be parallelized directly since it is applied to a non-associative function. Several techniques are applied in order to introduce parallelism, including partial evaluation and symbolic function representation. The derivation given here constitutes a semi-formal correctness proof, and it also brings out explicitly each of the ideas underlying the algorithm.