Contents of this page: Administrative matters | Technical presentations(Last updated 3rd May 2006.)
The ordering currently used is by the difference between "for" and "against" votes. We had some discussion of alternative orderings (perhaps "against" votes should carry more weight than "for"? is some lexicographic order on the pair of numbers of "for" and "against" votes more appropriate?), but the overall feeling was that members are happy for chair and secretary to decide. Members reaffirmed that the outcome of the voting process should not be made public, except in so far as the results are visible in the ordering of presentations; however, presentation proposers are welcome to ask for feedback on how their own proposal was received.
Should there be some kind of override of the scheduling procedure? It was suggested that the length of talks should affect the ranking, and that lower-ranked proposals might still be offered short slots, even if not full-length ones; but this suggestion was not universally supported. There was some concern about loss of audience attention during presentations, which is perhaps related to the prevalence of laptops. There was some support either for trying to have a meeting without laptops, or for turning off the internet connection during presentations.
Amidst the usual collection of strange characters and unfamiliar languages, we were blessed with an unusual abundance of delicacies. We were particularly impressed by the perfect conditions arranged for the study of conjunction on our see-day.
Interrupts are important for writing robust, modular programs, but are traditionally viewed as being difficult from a semantic perspective. In this talk we present a simple, formally justified, semantics for interrupts. Our approach is to consider a minimal high-level language and a minimal low-level machine with support for interrupts, give each a semantics, and then relate these semantics via a compiler. 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.See paper and slides. This is joint work with Joel Wright.
The last decade has seen a number of approaches to generic programming: PolyP, Functorial ML, `Scrap Your Boilerplate', Generic Haskell, `Generics for the Masses', etc. The approaches vary in sophistication and target audience: some propose full-blown programming languages, some suggest libraries, some can be seen as categorical programming methods. In this lecture, we shall compare the various approaches to generic programming in Haskell: we will introduce each method by means of example, and we will evaluate it along different dimensions (expressivity, ease of use, etc).
No abstract provided.
This talk gave an introduction to the uniform characterisation of Container data structures (eg, Lists) due to Abbott, Altenkirch and Ghani. Independently of the element type, a container is specified by a set of shapes and a function assigning to each shape a set of possible positions for elements. This gives a kind of 'power series' representation: a term in a container type is given by the pair of a shape and a function from its positions to elements. Containers come equipped with a notion of morphism capturing every mapping between containers which is polymorphic in elements. Containers are closed under constants, sums, products, identity, composition and functions with fixed domains, hence standard issue (co)inductive datatypes are readily coded as fixpoints of containers. We may thus develop useful generic equipment by abstracting parametrically over containers. A case in point is the 'one-hole context' construction, given uniformly by the derivative of the container. All of this equipment is directly representable in a dependently typed programming language, such as Epigram.See slides.
Fusion is a program transformation that combines adjacent computations, flattening structure and improving efficiency at the cost of clarity. Fission is the same transformation, in reverse: creating structure, ex nihilo. We explore the use of fission for program comprehension, that is, for reconstructing the design of a program from its implementation. We illustrate through rational reconstructions of the designs for three different C programs that count the words in a text file.The paper is to appear at MPC 2006.
A (partial) function f has a left inverse f-1 if f-1 . f = dom f. Consider simply typed lambda calculus where lambda expressions define partial functions from terms to terms. In this talk, we will propose a calculus which allows one to derive answers to the following questions: what is the left inverse of the K combinator, the B combinator, or C I (= λx y . y x)? In the future we hope to be able to deal with recursion and talk about, for example, the inverse of the function map.The research is currently in a very preliminary stage. On the other hand, the good news is that it does not seem to rely on any particular theory, which means that everyone can get involved!
One of the nicest features of lazy functional programming is the sequential composition of nonterminating computations. I'll describe how nonterminating state-transforming computations can be similarly composed, using stable properties (instead of finite data approximations) as a carrier, and how this can be extended to infinite sequences of such computations.
The Iterator pattern gives a clean interface for element-by-element access to a collection. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various functional iterations model one or other of these, but not both simultaneously. We argue that McBride's idioms, and in particular the corresponding traverse operator, model both simultaneously, and therefore capture the essence of the Iterator pattern. We present some axioms for traverse.A draft paper is available; this is joint work with Bruno Oliveira.
We present an algebraic derivation of Dijkstra's shortest path algorithm using Kleene algebra with tests, an instance of which are matrices over the familiar (min,+)-semiring. Using tests we can avoid special notation for matrix selection, as was employed in an earlier derivation by Backhouse et al. Also the structure of the derivation is different: it mimics closely the usual textbook correctness proof and the invariants involved. As a further application of the algebra a short derivation of the Warshall/Floyd algorithm is attached. Finally, Knuth's generalisation of Dijkstra's algorithm is posed as a challenge for algebraic derivation.
Slides are available; as are slides for a second talk A Survey of Command Algebra that was offered but not presented.
Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values.
It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation.
See scanned slides. This is joint work with Nils Anders Danielsson, Jeremy Gibbons and John Hughes.
No abstract provided.
No abstract provided.
We take a more a general approach to type classes than that of Haskell: Type classes are "kinds" of types. They can be defined via signatures (which essentially corresponds to Haskell-style type classes) or more generally via algebraic specifications. But they can also be defined using the traditional conctructions like products, sums or functions.We demonstrate two application of these principles. One is the definition of "dimension types", which allows type-safe programming in the realm of physical dimensions. The other is the specification of vectors and matrices, in particular special shapes like diagonal, tridiagonal, triangular matrices etc. The design is motivated by two goals:
- All relevant operations such as addition, multiplication etc shall be programmed only once, and the compiler shall generate for all kinds and combinations of shapes the optimial code automatically.
- Numerical algorithms shall be representable on the high level of compact vector-matrix operations (rather than with index calculations). This is demonstrated with two examples: LU-factoring and Fast Fourier Transformation.
No abstract provided.
No abstract provided.
The Eindhoven quantifier notation is systematic, unlike standard mathematicial notation. This has the major advantage that calculations with quantified expressions become more straightforward because the calculational rules need be given just once for a great variety of different quantifiers.The paper (joint work with Diethard Michaelis, accepted for presentation at MPC 2006) contains a number of additional examples.We demonstrated the ease of calculation with finite quantifications by considering two examples. The first was a simple warm-up exercise, using boolean equality as the quantifier. The second was a problem concocted by myself to demonstrate the techniques.
No abstract provided.
No abstract provided.
Building on the previous talk, I described the recent refinement from Containers to Indexed Containers, due to Altenkirch, Ghani, Hancock, myself and Morris. We index both the element types (with an input sort) and the structures we build from them (with an output sort). For example, vectors (lists of a given length) have a trivial input sort but a numeric output sort specifying length. The inductive families we use in Epigram all arise as fixpoints of indexed containers: these need not be taken as primitive, as they can be constructed from plain containers together with a proof that each subnode delivers the output sort required by the input sort of its parent. Containers in multiple kinds of element can readily be expressed as containers with a choice of input sort, so we may now construct new containers as fixpoints of old. We acquire a kit for constructing indexed containers which is sufficient to describe the dependent datatypes we use in Epigram, and which we plan to take as a basis for generic programming with dependent types.See slides.
I'll describe two new pretty functional programming problems that arise from an important industrial testing problem. The first problem - "optimal stateless search" - is to drive a terminating concurrent program (decorated with a conflict relation between pairs of actions from different threads) through exactly one execution from each conflict-equivalence class of schedules. The second problem - "optimal trace replay" - is to calculate an optimal strategy for using breakpoints to drive a thread forward to a chosen step of an execution trace.
The design of programs as the composition of smaller ones is a widespread approach to programming. In functional programming, this approach raises the necessity of creating a good amount of intermediate data structures with the only aim of passing data from one function to another. Using fusion techniques, it is possible to eliminate many of those intermediate data structures by an appropriate combination of the codes of the involved functions. In the standard case, no mention to the eliminated data structure remains in the code obtained from fusion. However, there are situations in which that data structure becomes an internal value manipulated by the fused program. This happens, for example, when paramorphisms are involved. We show, for example, that the result of fusing a paramorphism p with another function f may give as result a function that contains calls to f, and therefore contains the generation of data structures produced by f. Moreover, we show that in some cases the result of fusion may be less efficient than the original composition. We also investigate a generalized version of paramorphism which is a general recursion version of this program scheme. This study is strongly motivated by the development of HFusion, a fusion tool for Haskell programs.(Joint work with Facundo Domíngo.)