ICFP

A common reaction from people who hear about darcs, the source control system I created, is that it sounds like a great tool, but it is a shame that it is written in Haskell. People think that because darcs is written in Haskell it will be a slow memory ...

We describe the design and implementation of a full-featured Haskell development environment, based on Microsoft's extensible Visual Studio environment.Visual Haskell provides a number of features not found in existing Haskell development environments: ...

Haskell has proved itself to be a suitable implementation language for large software projects. Nevertheless, surprisingly few graphical end-user applications have been written in Haskell. Based on our experience with the development of the Bayesian ...

Some Lisp programs such as Emacs, but also the Linux kernel (when fully modularised) are mostly dynamic; i.e., apart from a small static core, the significant functionality is dynamically loaded. In this paper, we explore fully dynamic applications in ...

Haskell Server Pages (HSP) is a domain specific language, based on Haskell, for writing dynamic web pages. Its main features are concrete XML expressions as first class values, pattern-matching on XML, and a runtime system for evaluating dynamic web ...

Multi-core processors are coming, and we need ways to program them. The combination of purely-functional programming and explicit, monadic threads, communicating using transactional memory, looks like a particularly promising way to do so. This paper ...

Proof assistants based on dependent type theory are closely related to functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In this paper, we show how Agda, such a proof assistant, can be ...

The Curry-Howard isomorphism states that types are propositions and that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately, the type systems of today's functional languages cannot ...

Invertible programming occurs in the area of data conversion where it is required that the conversion in one direction is the inverse of the other. For that purpose, we introduce bidirectional arrows (bi-arrows). The bi-arrow class is an extension of ...

A type-indexed function is a function that is defined for each member of some family of types. Haskell's type class mechanism provides collections of open type-indexed functions, in which the indexing family can be extended by defining a new type class ...

Calculational developments of functional programs have been likened to conjuring tricks: enjoyable to watch but often a mystery as to how they are done. This pearl explains the trick. The aim is to give new calculations of two famous algorithms in ...

In the course of developing a web server for an embedded operating system, we had need of a filesystem which was small enough to alter to our needs and written in a high-level language so that we could show certain high assurance properties about its ...