Contents of this page: Administrative matters | Technical presentations(Last updated 17th December 2004.)
He hopes that the Group could then find an opportunity to present the book to Bob's widow, as a sign of our friendship and appreciation for Bob, as was Bob's wish.
Cunningly isolated from outside communication, the group had no choice but to exchange many a chat's worth of ideas: making its way through a coal tunnel of darkness and a maze of box hedges to emerge with a gravity-powered Revelation.
* not forgetting Maid Hilary
No abstract provided.
A generic function is defined by induction on the structure of types. The structure of a data type can be defined in several ways. For example, in PolyP a pattern functor gives the structure of a data type viewed as a fixed point, and in Generic Haskell a structural representation type gives an isomorphic type view of a data type in terms of sums of products. Depending on this generic view on the structure of data types, some generic functions are easier, more difficult, or even impossible to define. Furthermore, the efficiency of some generic functions can be improved by choosing a different view. This paper introduces generic views on data types, and shows why they are useful. Furthermore, it shows how to add new generic views to Generic Haskell, an extension of the functional programming language Haskell that supports the construction of generic functions. The separation between inductive definitions on type structure and generic views allows us to view many approaches to generic programming in a single framework.
We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive semantics of irreversible quantum computations realizable as quantum gates. QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings explicit. Strict programs are free of decoherence and hence preserve entanglement which is essential for quantum parallelism.(A paper is available.)
At the last meeting, I showed how to verify a compiler for a simple language with exceptions. I have since discovered how to calculate, as opposed to verify, an abstract machine for this language. The key step is the use of John Reynolds' "defunctionalisation" technique from 1972, which seems to have been largely forgotten by the program transformation community, but has recently been re-popularised by Olivier Danvy. In this talk I will review defunctionalisation, and show how it can be use to calculate an abstract machine for exceptions that is both simple and efficient.
A program may be transformed by specialising an interpreter for the language in which it is written. Efficiency of the transformed program is determined by the efficiency of the interpreter's dynamic operations; the efficiency of its static operations is irrelevant, since all will be ``specialised away''. This approach is automatic (as automatic as the specialiser is); general, in that it applies to all of the interpreter's input programs; and flexible, in that a wide range of program transformations are achievable since the transformed program inherits the style of the interpreter. The chief practical challenge is understanding cause and effect: How should one write the interpreter so that specialisation produces efficient transformed programs? The core of this paper is a series of examples, both positive and negative, showing how the way the interpreter is written can influence the removal of interpretational overhead, and thus the efficiency and size of the target programs obtained by specialisation.
One prediction for the Next Big Thing in mainstream software engineering is Model-Driven Architecture. This takes the current standard approach of manually implementing a UML design one step further: code is derived with some degree of automation from a platform-specific model, which is in turn derived from a platform-independent model. This kind of model transformation is a topic WG2.1 ought to be able to help with.My interest in this is that my group has recently been awarded a large grant for a project called CancerGRID, to develop software infrastructure for managing distributed cancer medical trials around the UK. My hope is that model-driven techniques can help in this development.
No abstract provided.
No abstract provided.
No abstract provided.
In the context of teaching algorithmic problem solving (see talk at Meeting #58) I was recently alerted to Sam Loyd's Chickens in the Corn problem.The problem is interesting because the combination of invariants and making progress in a well-formulated algorithm to solve the problem is non-trivial.
I would like to discuss a solution to the problem. Others may have better solutions, which I would like to hear about.
No abstract provided, but slides are available.
No abstract provided.
No abstract provided.
This talk will address my attempts to replace current semi-formal database schema design (à la Codd, based on normalization etc) by an inequational calculus based on simple (dually, injective) relations and their transposes. Many results generalize to other relations, the 'simple' ones being more relevant in practice just because database entities can always be modelled as finite simple relations. I find it much "simpler" to use this (pointfree) calculus than the standard theory. It includes a generic result which enables the refinement of recursive data models and which is the basis for a XML <-> SQL conversion tool which we are currently developing at Minho in Haskell/Strafunski.A copy of the slides is available.
No abstract provided, but the scanned slides are available.
Meta-S is a system for defining the cooperation and coordination of constraint solvers to attack hybrid constraint problems. Considering language evaluation mechanisms as constraint solvers and integrating these particular solvers into our system allows to combine arbitrary declarative languages and constraints. The talk exemplarily discusses these ideas for a logic language which yields a CLP language with support for solver cooperation.We use the strategy definition framework of Meta-S and define classical search strategies as well as new ones for an efficient evaluation of hybrid constraint logic programs.
This talk is a follow-up on the presentation Integration of Declarative and Constraint Programming at the 58th Meeting of the IFIP Working Group 2.1.
A paper is available.
No abstract provided.
We present an implementation of Oppen's pretty-printing solution in Haskell. The algorithm is linear in the size of the input, independent of the line width, uses limited look ahead, and has online behaviour.
No abstract provided, but slides are available.
At the Rome meeting (#58), I showed how the specification of the MEX function on games is derived. In this talk, I will show how the MEX sum is derived. The derivation centres on the observation that MEX numbers form a vector space over GF(2) (the field of booleans with xor as addition and conjunction as multiplication); the problem is solved by constructing a basis of this space.The talk describes recent joint work with Diethard Michaelis.
A paper is available.
No abstract provided, but slides are available.
The fictitious programming language fifol was designed anew for the purpose of a programming contest held in 2001. fifol (first in first out language) is similar to PostScript. fifol is a queue machine while PostScript is a stack machine. Operations are performed on items removed from the front end of the current fifo and the result is inserted to the rear end. Computation must be done solely in the queue, no memory storage was available.Some notes are available.In this talk, I will present my experience on programming in the rather peculiar and unfriendly language.
- Rules of the language fifol.
- Snapshots of executions for sample programs.
- Designing a program for computing square root of an integer.
We present techniques for representing typed abstract syntax trees in the presence of observable recursive structures. The need for this arose from the desire to cope with left-recursion in combinator based parsers. The techniques employed can be used in a much wider setting however, since it enables the inspection and transformation of any program structure, which contains internal references. The hard part of the work is to perform such analyses and transformations in a setting in which the Haskell type checker is still able to statically check the correctness of the program representations, and hence the type correctness of the transformed program.
No abstract provided.
No abstract provided.