title: Grammatical Framework

abstract: Grammatical Framework (GF) is a special-purpose functional language for defining grammars. It uses a Logical Framework (LF) for a description of abstract syntax, and adds to this a notation for defining concrete syntax. GF grammars themselves are purely declarative, but can be used both for linearizing syntax trees and parsing strings. GF can describe both formal and natural languages. The key notion of this description is a grammatical object, which is not just a string, but a record that contains all information on inflection and inherent grammatical features such as number and gender in natural languages, or precedence in formal languages. Grammatical objects have a type system, which helps to eliminate run-time errors in language processing. In the same way as a LF, GF uses dependent types in abstract syntax to express semantic conditions, such as well-typedness and proof obligations. Multilingual grammars, where one abstract syntax has many parallel concrete syntaxes, can be used for reliable and meaning-preserving translation. They can also be used in authoring systems, where syntax trees are constructed in an interactive editor similar to proof editors based on LF. While being edited, the trees can simultaneously be viewed in different languages. This paper starts with a gradual introduction to GF, going through a sequence of simpler formalisms till the full power is reached. The introduction is followed by a systematic presentation of the GF formalism and outlines of the main algorithms: partial evaluation and parser generation. The paper concludes by brief discussions of the Haskell implementation of GF, existing applications, and related work.


venue: jfp

title: "Proof, Language and Interaction, Essays in Honour of Robin Milner" by Gordon Plotkin, Colin Sterling and Mads Tofte (eds.), Foundations of Computing Series, MIT Press 2000


title: Knowledge Representation, Reasoning and Declarative Problem Solving by C. Baral, Cambridge University Press, 2003

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: Program Construction: Calculating Implementations from Specifications by R.C. Backhouse, John Wiley & Sons, 2004


title: Two-level types and parameterized modules

authors:
Tim Sheard
Emir Pasalic

abstract: In this paper, we describe two techniques for the efficient, modularized implementation of a large class of algorithms. We illustrate these techniques using several examples, including efficient generic unification algorithms that use reference cells to encode substitutions, and highly modular language implementations. We chose these examples to illustrate the following important techniques that we believe many functional programmers would find useful. First, defining recursive data types by splitting them into two levels: a structure defining level, and a recursive knot-tying level. Second, the use of rank-2 polymorphism inside Haskell's record types to implement a kind of type-parameterized modules. Finally, we explore techniques that allow us to combine already existing recursive Haskell data-types with the highly modular style of programming proposed here.


title: "An Introduction to Computing with Haskell" by Manuel M. T. Chakravarty and Gabrielle C. Keller, Pearson SprintPrint, 2002, ISBN 1 74009 404 2

abstract: The soft cover text An Introduction to Computing with Haskell with thirteen chapters, two appendices and an index on 145 pages of A4 is published on a 'print-on-demand' basis and available directly from the publishers in Sydney (at least in the sense that neither of the two large University bookshops I rang in Brisbane was able to find the book on their databases).Derived from lecture notes used in an introductory course at the University of New South Wales this book is attractively priced by Australian standards.At $AU 39.95 it retails for just slightly more than half the price of its nearest competitors.The relatively low price and a steering theme which embraces the elements and process of mathematical program analysis and reasoning are its distinguishing features.By the time they are finished, attentive readers should have soaked up a strong basis for a rational approach to computer programming and software design.In the words of the authors, the book sets out to introduce an 'absolute beginner' to computing including 'fundamental concepts of programming and simple forms of reasoning about programs'.That introduction mainly takes place in the computer programming language Haskell running under the Unix operating system.In pursuit of their aim Chakravarty and Keller eschew the usual heavy theory and dogma surrounding programming models in favour of a pedagogical framework composed of basic definitions built on informal discussion of some important ideas in programming.For example, the novice computer programmer is introduced to the idea and benefits of types as categories of values but doesn't have to grapple with category theory.Likewise, input and output are introduced as sequenceable actions expressed within the lazy paradigm of Haskell by the do notational idiom, but the theory of monoids and monads is ignored.Science does assume a fundamental role, however, as the student is quickly shown how to reason mathematically about program correctness and complexity through tools such as structural induction, the O notation and recurrence relations.Discussion around the main theme of this book is supported by a series of toy example programs, the most substantial of which are a video store database, a supermarket pricing program, a computer programming assignment auto-tester and an arithmetic expression evaluator.The auto-tester is a Unix shell script; the remaining examples being presented in Haskell.Exercises at the end of each chapter build on those examples and other issues.The GHCi compiler is also quickly introduced to the reader as a vehicle for Haskell programming.Let's turn now to a lecturer's check-list of the material covered (not in chapter order).Apart from the obligatory introduction and two chapters briefing the reader on Unix operating system basics and history, there are chapters covering types, control structures, recursion and input and output.Lists, higher order functions, user-defined data types, and tree structures fill out the remaining bread and butter chapters.There are also more advanced chapters on modularization and program decomposition, formal reasoning and work complexity.The chapter on trees covers sorted binary trees, AVL trees and tries.Another chapter introduces complexity analysis by developing the use of O notation through a discussion of that classic trio of sorting algorithms -insertion, merge and quicksort.


title: Reasoning About Program Transformations: Imperative Programming and Flow of Data by Jean-Francois Collard, Springer-Verlag, 2003


title: Composition of functions with accumulating parameters

authors:
Janis Voigtländer
Armin Kühnemann

abstract: Many functional programs with accumulating parameters are contained in the class of macro tree transducers. We present a program transformation technique that can be used to solve the efficiency problems due to creation and consumption of intermediate data structures in compositions of such functions, where classical deforestation techniques fail. To do so, given two macro tree transducers under appropriate restrictions, we construct a single macro tree transducer that implements the composition of the two original ones. The imposed restrictions are more liberal than those in the literature on macro tree transducer composition, thus generalising previous results.


title: "Practical Aspects of Declarative Languages" by Shriram Krishnamurthi and C. R. Ramakrishnan (eds.), LNCS 2257, Springer-Verlag, 2002. ISBN 3-540-43092-X


title: Type-safe cast

abstract: Comparing two types for equality is an essential ingredient for an implementation of dynamic types. Once equality has been established, it is safe to cast a value from one type to another. In a language with run-time type analysis, implementing such a procedure is fairly straightforward. Unfortunately, this naive implementation destructs and rebuilds the argument while iterating over its type structure. However, by using higher-order polymorphism, a casting function can treat its argument parametrically. We demonstrate this solution in two frameworks for ad-hoc polymorphism: intensional type analysis and Haskell type classes.


title: "Language-Based Security"

authors:
Martín Abadi
Greg Morrisett
Andrei Sabelfeld

abstract: Concepts and techniques from modern programming languages have much to offer to the security of computer systems. This special issue is devoted to research on those concepts and techniques. Over 60 active researchers working in this area were invited to contribute. In particular, a number of the participants of the Dagstuhl Seminar on Language-Based Security were encouraged to submit. Submitted articles were reviewed by 3–4 referees. As a result of the reviewing process, five articles were selected for inclusion in the special issue.


title: Models for machine learning and data mining in functional programming

abstract: The functional programming language Haskell and its type system are used to define and analyse the nature of some problems and tools in machine learning and data mining. Data types and type-classes for statistical models are developed that allow models to be manipulated in a precise, type-safe and flexible way. The statistical models considered include probability distributions, mixture models, function-models, time-series, and classification- and function-model-trees. The aim is to improve ways of designing and programming with models, not only of applying them.


title: Stack-based access control and secure information flow

authors:
Anindya Banerjee
David A. Naumann

abstract: Access control mechanisms are often used with the intent of enforcing confidentiality and integrity policies, but few rigorous connections have been made between information flow and runtime access control. The Java virtual machine and the .NET runtime system provide a dynamic access control mechanism in which permissions are granted to program units and a runtime mechanism checks permissions of code in the calling chain. We investigate a design pattern by which this mechanism can be used to achieve confidentiality and integrity goals: a single interface serves callers of more than one security level and dynamic access control prevents release of high information to low callers. Programs fitting this pattern would be rejected by previous flow analyses. We give a static analysis that admits them, using permission-dependent security types. The analysis is given for a class-based object-oriented language with features including inheritance, dynamic binding, dynamically allocated mutable objects, type casts and recursive types. The analysis is shown to ensure a noninterference property formalizing confidentiality and integrity.


title: Embedded interpreters

abstract: This is a tutorial on using type-indexed embedding/projection pairs when writing interpreters in statically-typed functional languages. The method allows (higher-order) values in the interpreting language to be embedded in the interpreted language and values from the interpreted language may be projected back into the interpreting one. This is particularly useful when adding command-line interfaces or scripting languages to applications written in functional languages. We first describe the basic idea and show how it may be extended to languages with recursive types and applied to elementary meta-programming. We then show how the method combines with Filinski's continuation-based monadic reflection operations to define an [lsquor]extensional[rsquor] version of the call-by-value monadic translation and hence to allow values to be mapped bidirectionally between the levels of an interpreter for a functional language parameterized by an arbitrary monad. Finally, we show how SML functions may be embedded into, and projected from, an interpreter for an asynchronous $\pi$ -calculus via an ‘extensional’ variant of a standard translation from $\lambda$ into $\pi$ .


title: Interfaces for stack inspection

authors:
Frédéric Besson
Thomas de Grenier de Latour
Thomas P. Jensen

abstract: Stack inspection is a mechanism for programming secure applications in the presence of code from various protection domains. Run-time checks of the call stack allow a method to obtain information about the code that (directly or indirectly) invoked it in order to make access control decisions. This mechanism is part of the security architecture of Java and the .NET Common Language Runtime. A central problem with stack inspection is to determine to what extent the local checks inserted into the code are sufficient to guarantee that a global security property is enforced. A further problem is how such verification can be carried out in an incremental fashion. Incremental analysis is important for avoiding re-analysis of library code every time it is used, and permits the library developer to reason about the code without knowing its context of deployment. We propose a technique for inferring interfaces for stack-inspecting libraries in the form of secure calling context for methods. By a secure calling context we mean a pre-condition on the call stack sufficient for guaranteeing that execution of the method will not violate a given global property. The technique is a constraint-based static program analysis implemented via fixed point iteration over an abstract domain of linear temporal logic properties.


title: Countdown: A case study in Origami programming

authors:
Richard S. Bird
Shin-Cheng Mu

abstract: Countdown is the name of a game in which one is given a list of source numbers and a target number, with the aim of building an arithmetic expression out of the source numbers to get as close to the target as possible. Starting with a relational specification we derive a number of functional programs for solving Countdown. These programs are obtained by exploiting the properties of the folds and unfolds of various data types, a style of programming Gibbons has aptly called origami programming. Countdown is attractive as a case study in origami programming both as an illustration of how different algorithms can emerge from a single specification, as well as the space and time trade-offs that have to be taken into account in comparing functional programs.


title: Correspondence assertions for process synchronization in concurrent communications

authors:
Eduardo Bonelli
Adriana B. Compagnoni
Elsa L. Gunter

abstract: High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types (Honda et al ., 1998). However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions (Clarke & Marrero, 1998; Gordon & Jeffrey, 2003b). The resulting type discipline augments the types of long-term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. This new type system can be used to check: source of information, whether data is propagated as specified across multiple parties, if there are unspecified communications between parties, and if the data being exchanged has been modified by the code in an unspecified way. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address shortcomings present in the pure theory of session types.


title: Deciding validity in a spatial logic for trees

authors:
Cristiano Calcagno
Luca Cardelli
Andrew D. Gordon

abstract: We consider a propositional spatial logic for finite trees. The logic includes $\A \Par \B$ (tree composition), $\A \,{\Guarantee}\, \B$ (the implication induced by composition), and $\Zero$ (the unit of composition). We show that the satisfaction and validity problems are equivalent, and decidable. The crux of the argument is devising a finite enumeration of trees to consider when deciding whether a spatial implication is satisfied. We introduce a sequent calculus for the logic, and show it to be sound and complete with respect to an interpretation in terms of satisfaction. Finally, we describe a complete proof procedure for the sequent calculus. We envisage applications in the area of logic-based type systems for semistructured data. We describe a small programming language based on this idea.


title: Meta-programming through typeful code representation

authors:
Chiyan Chen
Hongwei Xi

abstract: By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program efficiency and facilitate the construction of generic programs. However, meta-programming, especially in an untyped setting, is notoriously error-prone. In this paper, we aim at making meta-programming less error-prone by providing a type system to facilitate the construction of correct meta-programs. We first introduce some code constructors for constructing typeful code representation in which program variables are represented in terms of deBruijn indexes, and then formally demonstrate how such typeful code representation can be used to support meta-programming. With our approach, a particular interesting feature is that code becomes first-class values, which can be inspected as well as executed at run-time. The main contribution of the paper lies in the recognition and then the formalization of a novel approach to typed meta-programming that is practical, general and flexible.


title: A monadic analysis of information flow security with mutable state

authors:
Karl Crary
Aleksey Kliger
Frank Pfenning

abstract: We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic metalanguage. Thus, our logic deals with mutation explicitly, with impurity reflected in the types, in contrast to most higher-order security-typed languages, which deal with mutation implicitly via side-effects. More importantly, we also take a store-oriented view of security, wherein security levels are associated with elements of the mutable store. This view matches closely with the operational semantics of low-level imperative languages where information flow is expressed by operations on the store. An interesting feature of our analysis lies in its treatment of upcalls (low-security computations that include high-security ones), employing an “informativeness” judgment indicating under what circumstances a type carries useful information.


title: An intuitionistic [lambda]-calculus with exceptions

authors:
René David
Georges Mounier

abstract: We introduce a typed λ-calculus which allows the use of exceptions in the ML style. It is an extension of the system $AF_2$ of Krivine & Leivant (Krivine, 1990; Leivant, 1983). We show its main properties: confluence, strong normalization and weak subject reduction. The system satisfies the “the proof as program” paradigm as in $AF_2$ . Moreover, the underlined logic of our system is intuitionistic logic.


title: Skribe: a functional authoring language

authors:
Erick Gallesio
Manuel Serrano

abstract: This paper presents SKRIBE, a functional programming language for authoring documents, especially technical documents such as web pages, technical reports, and API documentation. Executing Skribe programs can produce documents in various formats, such as PostScript, PDF, HTML, Texinfo, or Unix man pages. That is, the very same Skribe program can be used to produce documents in different formats. Skribe is a full featured programming language whose syntax makes it look like a markup language à la HTML.For the sake of the example, here is the whole SKRIBE source code for the paragraph above:(p [This paper presents ,(Skribe), a functional programming language for authoring documents, especially technical documents such as web pages, technical reports, and API documentation. Executing Skribe programs can produce documents in various formats, such as PostScript, PDF, HTML, Texinfo, or Unix man pages. That is, the very same Skribe program can be used to produce documents in different formats. Skribe is a full featured programming language whose syntax makes it look like a markup language à la HTML.])SKRIBE can be downloaded at: http://www.inria.fr/mimosa/fp/Skribe.


title: Shared memory multiprocessor support for functional array processing in SAC

abstract: Classical application domains of parallel computing are dominated by processing large arrays of numerical data. Whereas most functional languages focus on lists and trees rather than on arrays, S A C is tailor-made in design and in implementation for efficient high-level array processing. Advanced compiler optimizations yield performance levels that are often competitive with low-level imperative implementations. Based on S A C, we develop compilation techniques and runtime system support for the compiler-directed parallel execution of high-level functional array processing code on shared memory architectures. Competitive sequential performance gives us the opportunity to exploit the conceptual advantages of the functional paradigm for achieving real performance gains with respect to existing imperative implementations, not only in comparison with uniprocessor runtimes. While the design of S A C facilitates parallelization, the particular challenge of high sequential performance is that realization of satisfying speedups through parallelization becomes substantially more difficult. We present an initial compilation scheme and multi-threaded execution model, which we step-wise refine to reduce organizational overhead and to improve parallel performance. We close with a detailed analysis of the impact of certain design decisions on runtime performance, based on a series of experiments.


title: VoDKA: Developing a Video-on-Demand Server using Distributed Functional Programming

authors:
Víctor M. Gulías
Miguel Barreiro
José Luis Freire

abstract: In this paper, we present some experience of using the concurrent functional language Erlang to implement a distributed video-on-demand server. For performance reasons, the server is deployed in a cheap cluster made from off-the-shelf components. The demanding system requirements, in addition to the complex and ever-changing domain, suggested a highly flexible and scalable architecture as well as a quite sophisticated control software. Functional programming played a key role in the development, allowing us to identify functional abstractions throughout the system. Using these building blocks, large configurations can be defined using functional and process composition, reducing the effort spent on adapting the system to the frequent changes in requirements. The server evolved from a prototype that was the result of a project supported by a regional cable company, and it is currently being used to provide services for real-world users. Despite our initial concerns, efficiency has not been a major issue.


title: The logic of demand in Haskell

authors:
William L. Harrison
Richard B. Kieburtz

abstract: Haskell is a functional programming language whose evaluation is lazy by default. However, Haskell also provides pattern matching facilities which add a modicum of eagerness to its otherwise lazy default evaluation. This mixed or “non-strict” semantics can be quite difficult to reason with. This paper introduces a programming logic, P -logic, which neatly formalizes the mixed evaluation in Haskell pattern-matching as a logic, thereby simplifying the task of specifying and verifying Haskell programs. In p -logic, aspects of demand are reflected or represented within both the predicate language and its model theory, allowing for expressive and comprehensible program verification.


title: Church numerals, twice!

abstract: This pearl explains Church numerals, twice. The first explanation links Church numerals to Peano numerals via the well-known encoding of data types in the polymorphic λ-calculus. This view suggests that Church numerals are folds in disguise. The second explanation, which is more elaborate, but also more insightful, derives Church numerals from first principles, that is, from an algebraic specification of addition and multiplication. Additionally, we illustrate the use of the parametricity theorem by proving exponentiation as reverse application correct.


title: Noninterference through flow analysis

authors:
Kohei Honda
Nobuko Yoshida

abstract: This paper proposes new syntactic inference rules which can directly extract information flow in a given typed process in the π-calculus. In the flow analysis, a flow in a process is captured as a chain of possible interactions which transform differences in behaviours from one part of its interface to another part of its interface. Polarity in types plays a fundamental role in the analysis, which is elucidated via examples. We show that this inductive flow analysis can be used for giving simple proofs of noninterference in the secrecy analyses for the π-calculus with linear/affine typing, including its concurrent, stateful extensions.


title: A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger

abstract: We present the Zen toolkit for morphological and phonological processing of natural languages. This toolkit is presented in literate programming style, in the Pidgin ML subset of the Objective Caml functional programming language. This toolkit is based on a systematic representation of finite state automata and transducers as decorated lexical trees. All operations on the state space data structures use the zipper technology, and a uniform sharing functor permits systematic maximum sharing as dags. A particular case of lexical maps is specially convenient for building invertible morphological operations such as inflected forms dictionaries, using a notion of differential word . As a particular application, we describe a general method for tagging a natural language text given as a phoneme stream by analysing possible euphonic liaisons between words belonging to a lexicon of inflected forms. The method uses the toolkit methodology by constructing a non-deterministic transducer, implementing rational rewrite rules, by mechanical decoration of a trie representation of the lexicon index. The algorithm is linear in the size of the lexicon. A coroutine interpreter is given, and its correctness and completeness are formally proved. An application to the segmentation of Sanskrit by sandhi analysis is demonstrated.


title: Typed lambda-calculi with one binder

abstract: Type theory was invented at the beginning of the twentieth century with the aim of avoiding the paradoxes which result from the self-application of functions. $\lambda$ -calculus was developed in the early 1930s as a theory of functions. In 1940, Church added type theory to his $\lambda$ -calculus giving us the influential simply typed $\lambda$ -calculus where types were simple and never created by binders (or abstractors). However, realising the limitations of the simply typed $\lambda$ -calculus, in the second half of the twentieth century we saw the birth of new more powerful typed $\lambda$ -calculi where types are indeed created by abstraction. Most of these calculi use two binders $\lambda$ and $\Pi$ to distinguish between functions (created by $\lambda$ -abstraction) and types (created by $\Pi$ -abstraction). Moreover, these calculi allow $\beta$ -reduction but not $\Pi$ -reduction. That is, $(\pi_{x:A}.B)C \rightarrow B[x:=C]$ is only allowed when $\pi$ is $\lambda$ but not when it is $\Pi$ . This means that, modern systems do not allow types to have the same instantiation right as functions. In particular, when $b$ has type $B$ , the type of $(\lambda_{x:A}.b)C$ is taken immediately to be $B[x:=C]$ instead of $(\Pi_{x:A}.B)C$ . Extensions of modern type systems with both $\Pi$ -reduction and type instantiation have appeared in (Kamareddine, Bloo and Nederpelt, 1999; Kamareddine and Nederpelt, 1996; Peyton-Jones and Meijer, 1997). This makes the $\lambda$ and $\Pi$ very similar and hence leads to the obvious question: why not use a unique binder instead of the $\lambda$ and $\Pi$ ? This makes more sense since already, versions of de Bruijn's Automath unified $\lambda$ and $\Pi$ giving more elegant systems. This paper studies the main properties of type systems with unified $\lambda$ and $\Pi$ .


title: Parallel functional programming in Eden

authors:
Rita Loogen
Yolanda Ortega-Mallén
Ricardo Peña-Marí

abstract: Eden extends the non-strict functional language Haskell with constructs to control parallel evaluation of processes. Although processes are defined explicitly, communication and synchronisation issues are handled in a way transparent to the programmer. In order to offer effective support for parallel evaluation, Eden's coordination constructs override the inherently sequential demand-driven (lazy) evaluation strategy of its computation language Haskell. Eden is a general-purpose parallel functional language suitable for developing sophisticated skeletons – which simplify parallel programming immensely – as well as for exploiting more irregular parallelism that cannot easily be captured by a predefined skeleton. The paper gives a comprehensive description of Eden, its semantics, its skeleton-based programming methodology – which is applied in three case studies – its implementation and performance. Furthermore it points at many additional results that have been achieved in the context of the Eden project.


title: Loci: a rule-based framework for parallel multi-disciplinary simulation synthesis

authors:
Edward A. Luke
Thomas George

abstract: We present a rule-based framework for the development of scalable parallel high performance simulations for a broad class of scientific applications (with particular emphasis on continuum mechanics). We take a pragmatic approach to our programming abstractions by implementing structures that are used frequently and have common high performance implementations on distributed memory architectures. The resulting framework borrows heavily from rule-based systems for relational database models, however limiting the scope to those parts that have obvious high performance implementation. Using our approach, we demonstrate predictable performance behavior and efficient utilization of large scale distributed memory architectures on problems of significant complexity involving multiple disciplines.


title: Staged computation with names and necessity

authors:
Aleksandar Nanevski
Frank Pfenning

abstract: Staging is a programming technique for dividing the computation in order to exploit the early availability of some arguments. In the early stages the program uses the available arguments to generate, at run time, the code for the late stages. A type system for staging should ensure that only well-typed expressions are generated, and that only expressions with no free variables are permitted for evaluation. In this paper, we present a calculus for staged computation in which code from the late stages is composed by splicing smaller code fragments into a larger context, possibly incurring capture of free variables. The type system ensures safety by tracking the names of free variables for each code fragment. The type system is based on the necessity operator □ from constructive modal logic, which we index with a set of names C. Our type □ C A classifies expressions of type A that belong to the late stage, and whose free names are in the set C.


title: Theoretical Pearls: A bargain for intersection types: a simple strong normalization proof

abstract: This pearl gives a discount proof of the folklore theorem that every strongly which can type any term.) The proof uses the perpetual reduction strategy which finds a longest path. This is a simplification over existing proofs that consider any longest reduction path. The choice of reduction strategy avoids the need for weakening or strengthening of type derivations. The proof becomes a bargain because it works for more intersection type systems, while being simpler than existing proofs.


title: Web programming in Scheme with LAML

abstract: Functional programming fits well with the use of descriptive markup in HTML and XML. There is also a good fit between S-expressions in Lisp and the XML data set. These similarities are exploited in LAML which is a software package for Scheme. LAML supports exact mirrors of the three variants of XHTML 1.0, SVG 1.0, and a number of more specialized XML languages. The mirrors are all synthesized from document type definitions (DTDs). Each element in a mirror is represented by a named function in Scheme. The mirror functions validate the XML document while it is generated. The validation is based on finite state automata automatically derived from the DTD.


title: Non-determinism analyses in a parallel-functional language

authors:
Ricardo Peña-Marí
Clara Segura

abstract: The parallel-functional language Eden has a non-deterministic construct, the process abstraction merge, which interleaves a set of input lists to produce a single non-deterministic list. Its non-deterministic behaviour is a consequence of its reactivity: it immediately copies to the output list any value appearing at any of the input lists. This feature is essential in reactive systems and very useful in some deterministic parallel algorithms. The presence of non-determinism creates some problems such that some internal transformations in the compiler must be disallowed. The paper describes several non-determinism analyses developed for Eden aimed at detecting the parts of the program that, even in the presence of a process merge, still exhibit a deterministic behaviour. A polynomial cost algorithm which annotates Eden expressions is described in detail. A denotational semantics is described for Eden and the correctness of all the analyses is proved with respect to this semantics.


title: Quantitative static analysis of distributed systems

authors:
Alessandra Di Pierro
Chris Hankin
Herbert Wiklicky

abstract: We introduce a quantitative approach to the analysis of distributed systems which relies on a linear operator based network semantics. A typical problem in a distributed setting is how information propagates through a network, and a typical qualitative analysis is concerned with establishing whether some information will eventually be transmitted from one node to another node in the network. The quantitative approach we present allows us to obtain additional information such as an estimation of the probability that some data is transmitted within a given interval of time. We formalise situations like this using a probabilistic version of a process calculus which is the core of KLAIM, a language for distributed and mobile computing based on interactions through distributed tuple spaces. The analysis we present exploits techniques based on Probabilistic Abstract Interpretation and is characterised by compositional aspects which greatly simplify the inspection of the nodes interaction and the detection of the information propagation through a computer network.


title: Educational Pearl: A Nanopass framework for compiler education

authors:
Dipanwita Sarkar
Oscar Waddell
R. Kent Dybvig

abstract: A compiler structured as a small number of monolithic passes is difficult to understand and difficult to maintain. The steep learning curve is daunting, and even experienced developers find that modifying existing passes is difficult and often introduces subtle and tenacious bugs. These problems are especially frustrating when the developer is a student in a compiler class. An attractive alternative is to structure a compiler as a collection of many fine-grained passes, each of which performs a single task. This structure aligns the implementation of a compiler with its logical organization, simplifying development, testing, and debugging. This paper describes the methodology and tools comprising a framework for constructing such compilers.


title: A parallel SML compiler based on algorithmic skeletons

authors:
Norman Scaife
Susumu Horiguchi
Greg Michaelson
Paul Bristow

abstract: Algorithmic skeletons are abstractions from common patterns of parallel activity which offer a high degree of reusability for developers of parallel algorithms. Their close association with higher order functions (HOFs) makes functional languages, with their strong transformational properties, excellent vehicles for skeleton-based parallel program development. However, using HOFs in this way raises substantial problems of identification of useful HOFs within a given application and of resource allocation on target architectures. We present the design and implementation of a parallelising compiler for Standard ML which exploits parallelism in the familiar $map$ and $fold$ HOFs through skeletons for processor farms and processor trees, respectively. The compiler extracts parallelism automatically and is target architecture independant. HOF execution within a functional language can be nested in the sense that one HOF may be passed and evaluated during the execution of another HOF. We are able to exploit this by nesting our parallel skeletons in a processor topology which matches the structure of the Standard ML source. However, where HOF arguments result from partially applied functions, free variable bindings must be identified and communicated through the corresponding skeleton hierarchy to where those arguments are actually applied. We describe the analysis leading from input Standard ML through HOF instantiation and backend compilation to an executable parallel program. We also present an overview of the runtime system and the execution model. Finally, we give parallel performance figures for several example programs, of varying computational loads, on the Linux-based Beowulf, IBM SP/2, Fujitsu AP3000 and Sun StarCat 15000 MIMD parallel machines. These demonstrate good cross-platform consistency of parallel code behaviour.


title: Lambda and pi calculi, CAM and SECD machines

abstract: We analyse machines that implement the call-by-value reduction strategy of the λ-calculus: two environment machines – CAM and SECD – and two encodings into the $\pi$ -calculus – due to Milner and Vasconcelos. To establish the relation between the various machines, we setup a notion of reduction machine and two notions of correspondences: operational – in which a reduction step in the source machine is mimicked by a sequence of steps in the target machine – and convergent – where only reduction to normal form is simulated. We show that there are operational correspondences from the λ-calculus into CAM, and from CAM and from SECD into the $\pi$ -calculus. Plotkin completes the picture by showing that there is a convergent correspondence from the λ-calculus into SECD.


title: Pure type systems with judgemental equality

abstract: In a typing system, there are two approaches that may be taken to the notion of equality. One can use some external relation of convertibility defined on the terms of the grammar, such as -convertibility; or one can introduce a judgement form for equality into the rules of the typing system itself. For quite some time, it has been an open problem whether the two systems produced by these two choices are equivalent. This problem is essentially the problem of proving that the Subject Reduction property holds in the system with judgemental equality. In this paper, we shall prove that the equivalence holds for all functional Pure Type Systems (PTSs). The proof essentially consists of proving the Church-Rosser Theorem for a typed version of parallel one-step reduction. This method should generalise easily to many typing systems which satisfy the Uniqueness of Types property.


title: Remarks on the equational theory of non-normalizing pure type systems

authors:
Gilles Barthe
Thierry Coquand

abstract: Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped $\lambda$ -abstractions (i.e. of the form $\lambda{x}.{M}$ ); and domain-free systems with typed $\lambda$ -abstractions (i.e. of the form $\lambda{x}{A}{M}$ ). Both flavours of systems are related by an erasure function $\er{.}$ that removes types from $\lambda$ -abstractions. Preservation of Equational Theory , which states the equational theories of both systems coincide through the erasure function, is a property of functional and normalizing PTSs. In this paper we establish that Preservation of Equational Theory fails for some non-normalizing PTSs, including the PTS with $\ast:\ast$. The gist of our argument is to exhibit a typable expression $Y_H$ whose erasure $\er{Y}$ is a fixpoint combinator, but which is not a fixpoint combinator itself.


title: Theoretical Pearl: A simple proof of a folklore theorem about delimited control

authors:
Dariusz Biernacki
Olivier Danvy

abstract: We formalize and prove the folklore theorem that the static delimited-control operators shift and reset can be simulated in terms of the dynamic delimited-control operators control and prompt. The proof is based on small-step operational semantics.


title: Functional Pearl: A program to solve Sudoku

abstract: There's no maths involved. You solve the puzzle with reasoning and logic. Advice on how to play Sudoku, The Independent Newspaper


title: Functional Pearls: Finding celebrities: A lesson in functional programming

authors:
Richard S. Bird
Sharon A. Curtis

abstract: The setting is a class on functional programming. There are four students, Anne, Jack, Mary and Theo.


title: Sound and complete models of contracts

authors:
Matthias Blume
David A. McAllester

abstract: Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. They did not, however, give a semantics of contracts. The lack of a semantics makes it impossible to define and prove soundness and completeness of the checking algorithm. (Given a semantics, a sound checker never reports violations that do not exist under that semantics; a complete checker is – in principle – able to find violations when violations exist.) Ideally, a semantics should capture what programmers intuitively feel is the meaning of a contract or otherwise clearly point out where intuition does not match reality. In this paper we give an interpretation of contracts for which we prove the Findler-Felleisen algorithm sound and (under reasonable assumptions) complete. While our semantics mostly matches intuition, it also exposes a problem with predicate contracts where an arguably more intuitive interpretation than ours would render the checking algorithm unsound. In our semantics we have to make use of a notion of safety (which we define in the paper) to avoid unsoundness. We are able to eliminate the “leakage” of safety into the semantics by changing the language, replacing the original version of unrestricted predicate contracts with a restricted form. The corresponding loss in expressive power can be recovered by making safety explicit as a contract. This can be done either in ad-hoc fashion or by including general recursive contracts . The addition of recursive contracts has far-reaching implications, deeply affecting the formulation of our model and requiring different techniques for proving soundness.


title: Consistency of the theory of contexts

authors:
Anna Bucalo
Furio Honsell
Marino Miculan
Ivan Scagnetto
Martin Hofmann

abstract: The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In this paper, we prove that this theory is consistent by building a model based on functor categories . By means of a suitable notion of forcing , we prove that this model validates Classical Higher Order Logic, the Theory of Contexts, and also (parametrised) structural induction and recursion principles over contexts. Our approach, which we present in full detail, should also be useful for reasoning on other models based on functor categories. Moreover, the construction could also be adopted, and possibly generalized, for validating other theories of names and binders.


title: Static analysis for path correctness of XML queries

authors:
Dario Colazzo
Giorgio Ghelli
Paolo Manghi
Carlo Sartiani

abstract: A part of a query that will never contribute data to the query answer should be regarded as an error. This principle has been recently accepted into mainstream XML query languages, but was still waiting for a complete treatment. We provide here a precise definition for this class of errors, and define a type system that is sound and complete, in its search for such errors, for a core language, under mild restrictions on the use of recursion in type definitions. In the process, we describe a dichotomy among existential and universal type systems, which is essential to understand some specific features of our type system.


title: Functional Pearl: Marble mingling

abstract: A bag (literally and mathematically!) of marbles is deemed to be mingled if all the colours of the marbles are different. Given a positive integer $k$ and a collection of $m$ marbles, our objective is to try and extract as many mingled bags as possible from the collection, where each bag contains exactly $k$ marbles.


title: Gencel: a program generator for correct spreadsheets

authors:
Martin Erwig
Robin Abraham
Steve Kollmansberger
Irene Cooperstein

abstract: A huge discrepancy between theory and practice exists in one popular application area of functional programming – spreadsheets. Although spreadsheets are the most frequently used (functional) programs, they fall short of the quality level that is expected of functional programs, which is evidenced by the fact that existing spreadsheets contain many errors, some of which have serious impacts. We have developed a template specification language that allows the definition of spreadsheet templates that describe possible spreadsheet evolutions. This language is based on a table calculus that formally captures the process of creating and modifying spreadsheets. We have developed a type system for this calculus that can prevent type, reference, and omission errors from occurring in spreadsheets. On the basis of the table calculus we have developed Gencel, a system for generating reliable spreadsheets. We have implemented a prototype version of Gencel as an extension of Excel.


title: Functional Pearls: Probabilistic functional programming in Haskell

authors:
Martin Erwig
Steve Kollmansberger

abstract: At the heart of functional programming rests the principle of referential transparency, which in particular means that a function f applied to a value x always yields one and the same value y=f(x) . This principle seems to be violated when contemplating the use of functions to describe probabilistic events, such as rolling a die: It is not clear at all what exactly the outcome will be, and neither is it guaranteed that the same value will be produced repeatedly. However, these two seemingly incompatible notions can be reconciled if probabilistic values are encapsulated in a data type.


title: Slideshow: functional presentations

authors:
Robert Bruce Findler
Matthew Flatt

abstract: Among systems for creating slide presentations, the dominant ones offer essentially no abstraction capability. Slideshow represents our effort over the last several years to build an abstraction-friendly slide system with PLT Scheme. We show how functional programming is well suited to the task of slide creation, we report on the programming contructs that we have developed for slides, and we describe our solutions to practical problems in rendering slides. We also describe experimental extensions to DrScheme that support a mixture of programmatic and WYSIWYG slide creation.


title: Introduction

abstract: The Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 19–21 2004 in Snowbird, Utah. The scope of ICFP includes all languages that encourage programming with functions, with topics ranging from principles to practice, foundations to features, and abstractions to applications. The program committee, which I chaired, selected 21 papers from 80 submissions for presentation at the conference. Afterwards, the program committee invited the authors of nine papers to submit extended versions for this special issue of JFP. The seven papers that appear in this volume were reviewed, revised, and accepted following standard Journal of Functional Programming procedures. Reflecting the scope of the conference, the papers cover the theoretical foundations, implementation, design, programming techniques, and applications of functional languages.


title: Monadic regions

authors:
Matthew Fluet
Greg Morrisett

abstract: Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, and proving their soundness is non-trivial. This paper shows that the complication is in principle unnecessary. In particular, we show that plain old parametric polymorphism, as found in Haskell, is all that is needed. We substantiate this claim by giving a type- and meaning-preserving translation from a variation of the region calculus of Tofte and Talpin to a monadic variant of System F with region primitives whose types and operations are inspired by (and generalize) the ST monad of Launchbury and Peyton Jones.


title: Phantom types and subtyping

authors:
Matthew Fluet
Riccardo Pucella

abstract: We investigate a technique from the literature, called the phantom-types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in Standard ML, can be used to enforce the subtyping relation, at least for first-order values. We show that this technique can be used to encode any finite subtyping hierarchy (including hierarchies arising from multiple interface inheritance). We formally demonstrate the suitability of the phantom-types technique for capturing first-order subtyping by exhibiting a type-preserving translation from a simple calculus with bounded polymorphism to a calculus embodying the type system of SML.


title: Functional Pearl: Enumerating the rationals

authors:
Jeremy Gibbons
David R. Lester
Richard S. Bird

abstract: Every lazy functional programmer knows about the following approach to enumerating the positive rationals: generate a two-dimensional matrix (an infinite list of infinite lists), then traverse its finite diagonals (an infinite list of finite lists).


title: A reflective functional language for hardware design and theorem proving

authors:
Jim Grundy
Thomas F. Melham
John W. O'Leary

abstract: This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself. The paper motivates and presents the syntax and type system of this language, which brings together a new combination of pattern-matching and reflection features targeted specifically at our application domain. It also gives an operational semantics based on a novel use of contexts as expression constructors, and it presents a scheme for compiling reFLect programs using the same context mechanism.


title: Efficient manipulation of binary data using pattern matching

authors:
Per Gustafsson
Konstantinos Sagonas

abstract: Pattern matching is an important operation in functional programs. So far, pattern matching has been investigated in the context of structured terms. This article presents an approach to extend pattern matching to terms without (much of a) structure such as binaries which is the kind of data format that network applications typically manipulate. After introducing the binary datatype and a notation for matching binary data against patterns, we present an algorithm that constructs a decision tree automaton from a set of binary patterns. We then show how the pattern matching using this tree automaton can be made adaptive, how redundant tests can be avoided, and how we can further reduce the size of the resulting automaton by taking interferences between patterns into account. Since the size of the tree automaton is exponential in the worst case, we also present an alternative new approach to compiling binary pattern matching which is conservative in space and analyze its complexity properties. The effectiveness of our techniques is evaluated using standard packet filter benchmarks and on implementations of network protocols taken from actual telecom applications.


title: Generics for the masses

abstract: A generic function is a function that can be instantiated on many data types to obtain data type specific functionality. Examples of generic functions are the functions that can be derived in Haskell, such as show , read , and ‘==’. The recent years have seen a number of proposals that support the definition of generic functions. Some of the proposals define new languages, some define extensions to existing languages. As a common characteristic none of the proposals can be made to work within Haskell 98: they all require something extra, either a more sophisticated type system or an additional language construct. The purpose of this paper is to show that one can, in fact, program generically within Haskell 98 obviating to some extent the need for fancy type systems or separate tools. Haskell's type classes are at the heart of this approach: they ensure that generic functions can be defined succinctly and, in particular, that they can be used painlessly. We detail three different implementations of generics both from a practical and from a theoretical perspective.


title: Finger trees: a simple general-purpose data structure

authors:
Ralf Hinze
Ross Paterson

abstract: We introduce 2-3 finger trees, a functional representation of persistent sequences supporting access to the ends in amortized constant time, and concatenation and splitting in time logarithmic in the size of the smaller piece. Representations achieving these bounds have appeared previously, but 2-3 finger trees are much simpler, as are the operations on them. Further, by defining the split operation in a general form, we obtain a general purpose data structure that can serve as a sequence, priority queue, search tree, priority search queue and more.


title: Regular expression filters for XML

abstract: XML data are described by types involving regular expressions. This raises the question of what language feature is convenient for manipulating such data. Previously, we have given an answer to this question by proposing regular expression pattern matching. However, since this construct is derived from ML pattern matching, it does not have an iteration functionality in itself, which makes it cumbersome to process data typed by Kleene stars. In this paper, we propose a novel programming feature regular expression filters . This construct extends the previous proposal by permitting pattern clauses to be closed under arbitrary regular expression operators. This yields many convenient programming idioms such as non-uniform processing of sequences and almost-copying of trees. We further develop a type inference mechanism that obtains (1) types for pattern variables that are locally precise with respect to the type of input values and (2) a type for the result of the whole filter expression that is also locally precise with respect to the types of the body expressions. We discuss how our construct is useful in the practice of XML processing and, in particular, how our type inference is crucial for avoiding changes of programs when types of data to be processed evolve frequently.


title: Educational Pearl: Automata via macros

abstract: Lisp programmers have long used macros to extend their language. Indeed, their success has inspired macro notations for a variety of other languages, such as C and Java. There is, however, a paucity of effective pedagogic examples of macro use. This paper presents a short, non-trivial example that implements a construct not already found in mainstream languages. Furthermore, it motivates the need for tail-calls, as opposed to mere tail-recursion, and illustrates how support for tail-call optimization is crucial to support a natural style of macro-based language extension.


title: Calculating PSSM probabilities with lazy dynamic programming

authors:
Ketil Malde
Robert Giegerich

abstract: Position-specific scoring matrices are one way to represent approximate string patterns, which are commonly encountered in the field of bioinformatics. An important problem that arises with their application is calculating the statistical significance of matches. We review the currently most efficient algorithm for this task, and show how it can be implemented in Haskell, taking advantage of the built-in non-strictness of the language. The resulting program turns out to be an instance of dynamic programming, using lists rather the typical dynamic programming matrix.


title: Making a fast curry: push/enter vs. eval/apply for higher-order languages

authors:
Simon Marlow
Simon L. Peyton Jones

abstract: Higher-order languages that encourage currying are typically implemented using one of two basic evaluation models: push/enter or eval/apply. Implementors use their intuition and qualitative judgements to choose one model or the other. Our goal in this paper is to provide, for the first time, a more substantial basis for this choice, based on our qualitative and quantitative experience of implementing both models in a state-of-the-art compiler for Haskell. Our conclusion is simple, and contradicts our initial intuition: compiled implementations should use eval/apply.


title: Featherweight generic confinement

authors:
Alex Potanin
James Noble
Dave Clarke
Robert Biddle

abstract: Existing approaches to object encapsulation either rely on ad hoc syntactic restrictions or require the use of specialised type systems. Syntactic restrictions are difficult to scale and to prove correct, while specialised type systems require extensive changes to programming languages. We demonstrate that confinement can be enforced cheaply in Featherweight Generic Java, with no essential change to the underlying language or type system. This result demonstrates that polymorphic type parameters can simultaneously act as ownership parameters and should facilitate the adoption of confinement and ownership type systems in general-purpose programming languages.


title: Multi-return function call

authors:
Olin Shivers
David Fisher

abstract: It is possible to extend the basic notion of “function call” to allow functions to have multiple return points. This turns out to be a surprisingly useful mechanism. This article conducts a fairly wide-ranging tour of such a feature: a formal semantics for a minimal $\lambda$ -calculus capturing the mechanism; motivating examples; monomorphic and parametrically polymorphic static type systems; useful transformations; implementation concerns and experience with an implementation; and comparison to related mechanisms, such as exceptions, sum-types and explicit continuations. We conclude that multiple-return function call is not only a useful and expressive mechanism, at both the source-code and intermediate-representation levels, but also quite inexpensive to implement.


title: Educational Pearl: Biological sequence similarity

abstract: Functional languages provide an excellent framework for formulating biological algorithms in a naive form and then transforming them into an efficient form. This helps biologists understand what matters about programming and brings functional programming into the realm of the practical. In this column, we present an example from our MSc course on bioinformatics and report on our experiences teaching functional programming in this context.


title: Type-safe run-time polytypic programming

abstract: Polytypic programming is a way of defining type-indexed operations, such as map, fold and zip, based on type information. Run-time polytypic programming allows that type information to be dynamically computed – this support is essential in modern programming languages that support separate compilation, first-class type abstraction, or polymorphic recursion. However, in previous work we defined run-time polytypic programming with a type-passing semantics. Although it is natural to define polytypic programs as operating over first-class types, such a semantics suffers from a number of drawbacks. This paper describes how to recast that work in a type-erasure semantics, where terms represent type information in a safe manner. The resulting language is simple and easy to implement – we present a prototype implementation of the necessary machinery as a small Haskell library.


title: Educational Pearl: 'Proof-directed debugging' revisited for a first-order version

abstract: Some 10 years ago, Harper illustrated the powerful method of proof-directed debugging for developing programs with an article in this journal. Unfortunately, his example uses both higher-order functions and continuation-passing style, which is too difficult for students in an introductory programming course. In this pearl, we present a first-order version of Harper's example and demonstrate that it is easy to transform the final version into an efficient state machine. Our new version convinces students that the approach is useful, even essential, in developing both correct and efficient programs.


title: Type-based confinement

authors:
Tian Zhao
Jens Palsberg
Jan Vitek

abstract: Confinement properties impose a structure on object graphs which can be used to enforce encapsulation properties. From a practical point of view, encapsulation is essential for building secure object-oriented systems as security requires that the interface between trusted and untrusted components of a system be clearly delineated and restricted to the smallest possible set of operations and data structures. This paper investigates the notion of package-level confinement and proposes a type system that enforces this notion for a call-by-value object calculus as well as a generic extension thereof. We give a proof of soundness of this type system, and establish links between this work and related research in language-based security.


title: A logical analysis of aliasing in imperative higher-order functions

authors:
Martin Berger
Kohei Honda
Nobuko Yoshida

abstract: Abstract We present a compositional programme logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data structures. The programme logic extends our earlier logic for alias-free imperative higher-order functions with new operators which serve as building blocks for clean structural reasoning about programms and data structures in the presence of aliasing. This has been an open issue since the pioneering work by Cartwright–Oppen and Morris twenty-five years ago. We illustrate usage of the logic for description and reasoning through concrete examples including a higher-order polymorphic Quicksort. The logical status of the new operators is clarified by translating them into (in)equalities of reference names.


title: MC2 A module calculus for Pure Type Systems

abstract: Abstract Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS) as their foundations. We are concerned with the issues involved in the development of large proofs in these provers such as namespace management, development of reusable proof libraries and separate verification. Although implementations offer many features to address them, few theoretical foundations have been laid for them up to now. This is a problem as features dealing with modularity may have harmful, unsuspected effects on the reliability or usability of an implementation. In this paper, we propose an extension of Pure Type Systems with a module system, $\mathcal{MC}_2$ , adapted from SML-like module systems for programming languages. This system gives a theoretical framework addressing the issues mentioned above in a quite uniform way. It is intended to be a theoretical foundation for the module systems of proof-assistants such as Coq or Agda. We show how reliability and usability can be formalized as metatheoretical properties and prove they hold for $\mathcal{MC}_2$ .


title: On one-pass CPS transformations

authors:
Olivier Danvy
Kevin Millikin
Lasse R. Nielsen

abstract: Abstract We bridge two distinct approaches to one-pass CPS transformations, i.e, CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is independently due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a reduction semantics for the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use three tools: Reynolds's defunctionalization and its left inverse, refunctionalization; a special case of fold–unfold fusion due to Ohori and Sasano, fixed-point promotion; and an implementation technique for reduction semantics due to Danvy and Nielsen, refocusing. This work is directly applicable to transforming programs into monadic normal form.


title: Recursive type generativity

abstract: Abstract Existential types provide a simple and elegant foundation for understanding generative abstract data types of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found that the traditional existential account of type generativity does not work well in the presence of mutually recursive module definitions. The key problem is that, in recursive modules, one may wish to define an abstract type in a context where a name for the type already exists, but the existential type mechanism does not allow one to do so. We propose a novel account of recursive type generativity that resolves this problem. The basic idea is to separate the act of generating a name for an abstract type from the act of defining its underlying representation. To define several abstract types recursively, one may first ‘forward-declare’ them by generating their names, and then supply each one's identity secretly within its own defining expression. Intuitively, this can be viewed as a kind of backpatching semantics for recursion at the level of types . Care must be taken to ensure that a type name is not defined more than once, and that cycles do not arise among ‘transparent’ type definitions. In contrast to the usual continuation-passing interpretation of existential types in terms of universal types, our account of type generativity suggests a destination-passing interpretation. Briefly, instead of viewing a value of existential type as something that creates a new abstract type every time it is unpacked, we view it as a function that takes as input a pre-existing undefined abstract type and defines it. By leaving the creation of the abstract type name up to the client of the existential, our approach makes it significantly easier to link abstract data types together recursively.


title: A monadic framework for delimited continuations

authors:
R. Kent Dybvig
Simon L. Peyton Jones
Amr Sabry

abstract: Abstract Delimited continuations are more expressive than traditional abortive continuations and they apparently require a framework beyond traditional continuation-passing style (CPS). We show that this is not the case: standard CPS is sufficient to explain the common control operators for delimited continuations. We demonstrate this fact and present an implementation as a Scheme library. We then investigate a typed account of delimited continuations that makes explicit where control effects can occur. This results in a monadic framework for typed and encapsulated delimited continuations, which we design and implement as a Haskell library.


title: Preface

authors:
Matthew Flatt
Benjamin C. Pierce

abstract: The Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP) was held in September, 2005, in Tallinn, Estonia; Benjamin Pierce chaired the program committee. After the conference, extended versions of some of the presented papers were solicited for this special issue of JFP. All submitted papers were reviewed following standard JFP procedures and four were ultimately accepted; they form the body of this special issue.


title: An extended comparative study of language support for generic programming

authors:
Ronald Garcia
Jaakko Järvi
Andrew Lumsdaine
Jeremy G. Siek
Jeremiah Willcock

abstract: Abstract Many modern programming languages support basic generics, sufficient to implement type-safe polymorphic containers. Some languages have moved beyond this basic support, and in doing so have enabled a broader, more powerful form of generic programming. This paper reports on a comprehensive comparison of facilities for generic programming in eight programming languages: C++, Standard ML, Objective Caml, Haskell, Eiffel, Java, C# (with its proposed generics extension), and Cecil. By implementing a substantial example in each of these languages, we illustrate how the basic roles of generic programming can be represented in each language. We also identify eight language properties that support this broader view of generic programming: support for multi-type concepts, multiple constraints on type parameters, convenient associated type access, constraints on associated types, retroactive modeling, type aliases, separate compilation of algorithms and data structures, and implicit argument type deduction for generic algorithms. We find that these features are necessary to avoid awkward designs, poor maintainability, and painfully verbose code. As languages increasingly support generics, it is important that language designers understand the features necessary to enable the effective use of generics and that their absence can cause difficulties for programmers.


title: Monadic augment and generalised short cut fusion

authors:
Neil Ghani
Patricia Johann

abstract: Abstract Monads are commonplace programming devices that are used to uniformly structure computations; in particular, they are often used to mimic the effects of impure features such as state, error handling, and I/O. This paper further develops the monadic programming paradigm by investigating the extent to which monadic computations can be optimised by using generalisations of short cut fusion to eliminate monadic structures whose sole purpose is to “glue together” monadic program components. Ghani, Uustalu, and Vene have recently shown that every inductive type has an associated build combinator and an associated short cut fusion law. They have also used the notion of a parameterised monad to describe those monads that give rise to inductive types, and have shown that the standard augment combinators and cata / augment fusion rules for algebraic data types can be generalised to fixed points of all parameterised monads. We revisit these augment combinators and generalised short cut fusion rules for such types but consider them from a functional programming perspective, rather than a categorical one. In addition to making the category-theoretic ideas of Ghani, Uustalu, and Vene more easily accessible to a wider audience of functional programmers, we demonstrate their practical applicability by developing nontrivial application programs and performing modest benchmarking on them. We also show how the cata / augment rules can serve as the basis for deriving additional generic fusion laws, thus opening the way for an algebra of fusion . Finally, we offer deep theoretical insights, arguing that the augment combinators are monadic in nature, and thus that the cata / build and cata / augment rules are arguably the best generally applicable fusion rules obtainable.


title: Mechanizing metatheory in a logical framework

authors:
Robert Harper
Daniel R. Licata

abstract: Abstract The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the syntactic and deductive apparatus of a system is encoded as the canonical forms of associated LF types; an encoding is correct ( adequate ) if and only if it defines a compositional bijection between the apparatus of the deductive system and the associated canonical forms. Given an adequate encoding, one may establish metatheoretic properties of a deductive system by reasoning about the associated LF representation. The Twelf implementation of the LF logical framework is a convenient and powerful tool for putting this methodology into practice. Twelf supports both the representation of a deductive system and the mechanical verification of proofs of metatheorems about it. The purpose of this article is to provide an up-to-date overview of the LF λ-calculus, the LF methodology for adequate representation, and the Twelf methodology for mechanizing metatheory. We begin by defining a variant of the original LF language, called Canonical LF , in which only canonical forms (long βη-normal forms) are permitted. This variant is parameterized by a subordination relation , which enables modular reasoning about LF representations. We then give an adequate representation of a simply typed λ-calculus in Canonical LF, both to illustrate adequacy and to serve as an object of analysis. Using this representation, we formalize and verify the proofs of some metatheoretic results, including preservation, determinacy, and strengthening. Each example illustrates a significant aspect of using LF and Twelf for formalized metatheory.


title: What is the meaning of these constant interruptions?

authors:
Graham Hutton
Joel J. Wright

abstract: Abstract Asynchronous exceptions, or interrupts , are important for writing robust, modular programs, but are traditionally viewed as being difficult from a semantic perspective. In this article, we present a simple, formally justified, semantics for interrupts. Our approach is to show how a high-level semantics for interrupts can be justified with respect to a low-level implementation, by means of a compiler and its correctness theorem. In this manner we obtain two different perspectives on the problem, formally shown to be equivalent, which gives greater confidence in the correctness of our semantics.


title: The Haskell School of Expression by Hudak Paul, Cambridge Univerity Press, 20001


title: Practical type inference for arbitrary-rank types

authors:
Simon L. Peyton Jones
Dimitrios Vytiniotis
Stephanie Weirich
Mark Shields

abstract: Abstract Haskell's popularity has driven the need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types – that is, functions that take polymorphic functions as their arguments. Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code. However, the choice of just what annotations are required, and what changes are required in the type system and its inference algorithm, has been an ongoing topic of research. We take as our starting point a λ-calculus proposed by Odersky and Läufer. Their system supports arbitrary-rank polymorphism through the exploitation of type annotations on λ-bound arguments and arbitrary sub-terms. Though elegant, and more convenient than some other proposals, Odersky and Läufer's system requires many annotations. We show how to use local type inference (invented by Pierce and Turner) to greatly reduce the annotation burden, to the point where higher-rank types become eminently usable. Higher-rank types have a very modest impact on type inference. We substantiate this claim in a very concrete way, by presenting a complete type-inference engine, written in Haskell, for a traditional Damas-Milner type system, and then showing how to extend it for higher-rank types. We write the type-inference engine using a monadic framework: it turns out to be a particularly compelling example of monads in action. The paper is long, but is strongly tutorial in style. Although we use Haskell as our example source language, and our implementation language, much of our work is directly applicable to any ML-like functional language.


title: SMIL 2.0 Interactive Multimedia for Web and Mobile Devices by C. A. Dick Bulterman and Lloyd Rutledge, Springer X.media.publishing, 2004, 440pp, ISBN 3-540-20234-X

abstract: This is the first textbook containing a complete, in depth description of SMIL.SMIL is an XML language, promulgated by the World Wide Web Consortium, for multimedia authoring.SMIL may be used to create sophisticated multi and hyper-media artifacts by means of the temporal and spatial integration of existing media items, and by defining certain forms of reactivity among such media items.SMIL is typically used for "rich media"/multimedia presentations which integrate streaming audio and video with images, text or any other media type.In common with all XML languages, SMIL is declarative in nature and permits the author to ascribe values to attribute names, such as duration, start, and so forth, which serve to define the behaviour of the items comprising the multimedia artifact.Despite considerable interest in SMIL, especially in the academic community, there has until now been a relative dearth of comprehensive, user-oriented material dealing with the language.This monograph fills the gap admirably.It is written by two of the foremost experts on SMIL, both of whom were intimately involved in the development of both SMIL 1.0 and SMIL 2.0.The authors, appropriately, claim that the book is designed for three audiences: existing SMIL users who need more information, new SMIL authors, and multimedia developers; the book more than adequately meets the needs of these three different audiences.The book is not intended to introduce the concepts of multimedia or, more specifically, multimedia timing concepts.The book certainly achieves its aims of meeting the needs of newcomers and more seasoned developers.In this regard, a particular strength of the volume is the diversity of examples used to describe features of the SMIL language.The newcomer is presented with six examples introduced in Chapter 1 of the book, where they are used to describe the power of SMIL and its diversity of applicability.A number of these examples reappear later at various stages of the book used later on when describing specific SMIL features.The book encourages a hands-on approach to learning SMIL.Part One of the book, comprising the three initial chapters, provides a complete overview enough features of SMIL that the reader will be in a position to modify existing SMIL presentations and create his or her own new ones once this material has been assimilated.It is noteworthy that in addition to the complete stand-alone presentations, the book contains numerous illustrative code fragments, many of which could be used as templates by the reader when creating her/his own scripts.In this regard, however, it is disappointing that the book does not include a CD ROM containing the examples and code fragments and a SMIL player.This is particularly so as the website to which the reader is referred for this purpose appears to lack the section containing the demos and code in the book!Some of these are on the website, but one has to dig deep to find them.Even so, the website will be of little help to the insomniac reader crossing the Atlantic, who wishes to pass the time by adapting one of the book's presentations.Parts Two and Three of the book provide a more structured, thorough treatment of basic and more advanced SMIL constructs.Once the multimedia author moves away from all but the simplest specifications, authoring becomes a far from simple task, and in all but its most


title: Warnings for pattern matching

abstract: Abstract We examine the ML pattern-matching anomalies of useless clauses and non-exhaustive matches. We state the definition of these anomalies, building upon pattern matching semantics, and propose a simple algorithm to detect them. We have integrated the algorithm in the Objective Caml compiler, but we show that the same algorithm is also usable in a non-strict language such as Haskell. Or-patterns are considered for both strict and non-strict languages.


title: Inductive Synthesis of Functional Programs by U. Schmid, Springer Verlag, 2003, 420pp, ISBN 3540401741

abstract: Programming" framework, Yampa.If you like little languages, you'll appreciate how useful Haskell is for embedded domain specific languages.It may be even more useful now that Template Haskell is in the works.


title: Type sharing constraints and undecidability

abstract: Abstract Let ${\cal A}$ be a set of modules and parameterized modules including type sharing constraint specifications. We prove that determining the set of the effective modules described by ${\cal A}$ is undecidable. As a consequence, type sharing constraints are proved to be not always avoidable by constructive transformations.


title: Engineering Software Correctness

abstract: Abstract Design and quality are fundamental themes in engineering education. Functional programming builds software from small components, a central element of good design, and facilitates reasoning about correctness, an important aspect of quality. Software engineering courses that employ functional programming provide a platform for educating students in the design of quality software. This pearl describes experiments in the use of ACL2, a purely functional subset of Common Lisp with an embedded mechanical logic, to focus on design and correctness in software engineering courses. Students find the courses challenging and interesting. A few acquire enough skill to use an automated theorem prover on the job without additional training. Many students, but not quite a majority, find enough success to suggest that additional experience would make them effective users of mechanized logic in commercial software development. Nearly all gain a new perspective on what it means for software to be correct and acquire a good understanding of functional programming.


title: Acute: High-level programming language design for distributed computation

authors:
Peter Sewell
James J. Leifer
Keith Wansbrough
Francesco Zappa Nardelli
Mair Allen-Williams
Pierre Habouzit
Viktor Vafeiadis

abstract: Abstract Existing languages provide good support for typeful programming of stand-alone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper, we discuss programming-language support for such systems, focussing on their typing and naming issues. We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately built programs. The main features are (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type safety of associated values, for example, values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility. These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language run-time from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.


title: Programming Languages and Operational Semantics by Fernández Maribel, King's College Publications, 2004, ISBN 0954300637


title: Understanding functional dependencies via constraint handling rules

authors:
Martin Sulzmann
Gregory J. Duck
Simon L. Peyton Jones
Peter J. Stuckey

abstract: Abstract Functional dependencies are a popular and useful extension to Haskell style type classes. We give a reformulation of functional dependencies in terms of Constraint Handling Rules (CHRs). In previous work, CHRs have been employed for describing user-programmable type extensions in the context of Haskell style type classes. Here, we make use of CHRs to provide for the first time a concise result that under some sufficient conditions, functional dependencies allow for sound, complete and decidable type inference. The sufficient conditions imposed on functional dependencies can be very limiting. We show how to safely relax these conditions and suggest several sound extensions of functional dependencies. Our results allow for a better understanding of functional dependencies and open up the opportunity for new applications.


title: An object-oriented calculus with term constraints

abstract: Abstract Safety has become a fundamental requirement in all aspects of computer systems. Object-oriented calculi, such as Castagna's λ&-calculus and its variants (Castagna, 1997) ensure type safety in environments based on the distinguished object-oriented paradigm. Although for safety reasons object invariance and operation specifications are getting widely employed in all stages of the engineering process, they are not supported by these calculi. In this paper, a new calculus is presented which supports term (value) constraints besides the key object-oriented mechanisms (class types, inheritance, overloading with multiple dispatch and late binding). We also show how a type with constraints may realise a role, another useful object-oriented modelling element. The soundness of the type system and the confluence of the notion of reduction of the calculus are considered. The contribution also discusses computability issues partially arising from the use of first-order logic to formalise the constraints.


title: Verification of Reactive Systems by Klaus Schneider Springer Verlag, 2003, 600pp, ISBN 3-540-00296-0

abstract: This book discusses four approaches typically used for the verification of reactive systems.However, the book is not merely a description of these four formalisms, since the existing connections between these techniques are also established.In addition, complexity results associated with each method are presented, together with discussions about good features and difficulties that must be faced when dealing with each particular technique.It cannot be said that this is a practical book.On the contrary, this book presents fundamental theory that every researcher on formal methods should be familiar with.Therefore, the audience for this book is mainly theoreticians with some background in automata theory and logics.They will enjoy discovering the underlying interrelations among the different approaches presented along the book.Almost all the results presented encompass useful descriptions and explanations, which makes the reading more fluent, especially when the reader doesn't want to go into the details of a specific proof or result.It must be said that the notation used by the authors does not always follow the established notation, as used in the original research papers, for instance.This fact increases the difficulty of reading the text since some extra time must be invested in getting accustomed to the new notation.Independently from the contents, the readability of the book is sometimes degraded due to the presence of some typographical errors, but they do not prevent the reader from understanding the topics of the text.Looking into the contents, the book starts with a marvelous introduction where, first of all, a classification of formal methods and systems can be found.The ancient (maybe not so ancient) history of logic theories and verification techniques is narrated.This part of the book, in addition to being a very nice introductory description of the formalisms that will be described in the rest of the book, is also an advertisement to the reader of the theoretical point of view that will be used through the book, which continuously will frame the equivalences and relations among the four formalisms.The book includes a remarkable bibliography section.This is not only notable for its contents, but also for how they are cited.Bibliographic references are perfectly integrated into the book itself, and can be especially useful in the introduction and in the appendixes, where the topics are not completely developed and the reader is referred to related and perhaps more detailed works.Before considering the main contents of the book, the second chapter presents a unified specification language which combines µ-calculus, ω-automata, temporal logics and predicate logics.This unified language provides the author with an unified notation for defining each formalism in the rest of the book and for showing the formal links between the different approaches.Notions such as Kripke structures, fairness, simulations, bisimulations and products of structures are introduced and will be used in several sections of the book.The organization of the main chapters of the book is as follows: Chapter 3 is devoted to the first formalism, the µ-calculus; then, Chapter 4 deals with ω-automata, the following chapter describes temporal logics (in particular, variants of CTL) and finally, in Chapter 6, predicate logics are used for the verification of reactive systems.Note that although these four chapters


title: Spreadsheet functional programming

abstract: Abstract The functional programming community has shown some interest in spreadsheets, but surprisingly no one seems to have considered making a standard spreadsheet, such as Excel, work with a standard functional programming language, such as Haskell. In this paper, we show one way that this can be done. Our hope is that by doing so, we might get spreadsheet programmers to give functional programming a try.


title: Dependent ML An approach to practical programming with dependent types

abstract: Abstract We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language ${\cal L}$ that is completely separate from run-time programs, leading to the DML( ${\cal L}$ ) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions.


title: Control reduction theories: the benefit of structural substitution

authors:
Zena M. Ariola
Hugo Herbelin

abstract: Abstract The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a continuation. To the contrary, the control calculus, developed by the authors, distinguishes between jumps and terms . This alternative calculus, which derives from Parigot's λμ-calculus, works by direct structural substitution of evaluation contexts. We review and revisit the legacy theories of control and argue that provides an observationally equivalent but smoother theory. In an additional note contributed by Matthias Felleisen, we review the story of the birth of control calculi during the mid- to late-eighties at Indiana University.


title: A type system with usage aspects

authors:
David Aspinall
Martin Hofmann
Michal Konecný

abstract: Abstract Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a “read-only” context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konečn'y (In TYPES 2002 workshop, Nijmegen, Proceedings , Springer-Verlag, 2003).