Foundations of Programming Meetings
School of Computer Science and ITUniversity of Nottingham
The Foundations of Programming group holds regular research meetings. The meetings last around an hour, and are intended to be a friendly forum for discussion and exchange of ideas. Most meetings take the form of a talk by a group member or an invited speaker, but we also have various kinds of discussion sessions. The meetings are open to everyone, not just members of the group. Please contact Graham Hutton if you are interested in visiting the group and giving a talk.
Details of previous years meetings are also available: 1995; 1996; 1997; 1998; 1999; 2000; 2001; 2002.
Details of recent and upcoming meetings are given below.
This talk shows how to develop a Haskell program that solves the
numbers game from Countdown, the popular afternoon quiz show on
Channel 4. The aim wasn't to produce solutions as fast as possible
(although in absolute terms the final program actually performs rather
well), but rather to show how the program itself could be developed in
a systematic way in conjunction with a proof of its correctness. The
talk will be aimed at a general audience - everyone is welcome to come
along and find out how to beat Carol Vorderman at her own game!
We give a simple but precise explanation of the basic method for
compiling exceptions, by presenting a compiler for a small language with
exceptions. There is a proof of correctness of the compiler in
the
paper but it will not be covered in the talk.
Quantum computers can offer increased performance in a range of problems
over traditional (classical) computers. Important algorithms are Peter Shor's
1994 quantum factorisation algorithm, which offers an exponential speed
up, and Grovers 1996 quantum database search, which offers a quadratic
speed up. Due to the counter-intuitiveness of quantum mechanics, algorithms
that use these techniques and out perform classical algorithms are difficult
to formulate.
Logics are powerful tools with which to reason about the behaviour of AI
agents. A particular logic may provide an agent with an internal language
with which it can represent and reason about the world, and act based upon
its internal manipulation of this language. We can also use logics to reason
about the behaviour of agents from an external perspective.
I survey several common approaches taken by researchers in artificial
intelligence and compare these to philosophically motivated accounts. In
selecting the most desirable features from a variety of differing accounts,
I sketch a direction for future work in the area.
Functional polytypic programming is one way of doing generic programming in
the functional world. In this talk, I will briefly talk about generic
programming in general and more about functional polytypic programming
(eg. Generic Haskell) in particular, and underline the latter's problem to
cope with data abstraction. I will suggest a possible theoretical solution
that draws upon concepts of Category-Theory and, if time permits, discuss
other approaches based on the Visitor design pattern and its cousin, the
many-sorted fold. I hope to be able to crack a few jokes along the way
The aim of the talk is to present a modern outlook on the relationship
between propositional modal and classical first-order logics and to show
how this outlook gives rise to a new research area in logic, guarded
logics. Guarded logics retain all nice computational properties of
modal logics, while extending their expressive power. They have
recently been found of significant practical value, particularly in the
field of database queries.
This talk will review some aspects of the recent research on
coalgebras and modal logic. Coalgebras being the categorical dual of
algebras, we will be guided by (and make precise in several ways) the
idea that modal logic is dual to equational logic.
Predicting the space-time behaviour of functional programs is more
complicated than for procedural languages. This talk will show how to
measure the space-time usage of simple functions and how implementation
and evaluation order can affect usage and so be used to improve the
efficiency of functions. I will also briefly mention using recursion
operators to tackle this problem.
I shall speak of an application of recursive conditions to solving the
inclusion problem in algebra. The inclusion problem of a class of
algebras asks whether a finite algebra belongs to the class. An
example of such a problem is checking that a finite group is
commutative (i.e. belongs to the class of all commutative
groups). Depending on the class in question, the problem can be
undecidable, or polynomial (with respect to the size of an algebra),
of NP-complete (I have found several examples), or provably
non-polynomial.
In this talk, I shall speak of "good" classes, i.e. classes with a
polynomial inclusion problem. A traditional way of defining classes of
algebras is with logical conditions. For example, commutativity is
represented by the logical condition xy=yx. It can easily be proved
that if a class is defined by a finite set of logical conditions then
its inclusion problem is polynomial. However, the reverse is not
true. Not all classes with a polynomial inclusion problem can be
defined by a finite set of logical conditions. Moreover, many
important classes fall in this gap: they have a polynomial inclusion
problem but cannot be defined by a finite set of logical
conditions. Therefore, I have created a new form of logical conditions
for defining classes of algebras. These new logical conditions can be
recursive, and thanks to this can define more classes of algebras than
standard logical conditions.
I shall describe the recursive logical conditions and discuss their
possible applications.
In \cite{Kra2002} we develop a syntax-only classification of
evolutionary
algorithms, particularly, the so called Memetic Algorithms(MAs).
When ``syntactic sugar'' is added to our model, we are able to
investigate the Polynomial Local Search (PLS) complexity of Memetic
Algorithms. In this talk we enunciate the PLS-Completeness of not just
one PLS problem but of whole
classes of problems associated with MAs applied to the TSP.
These classes of problems arise when a range of mutation,
crossover and local search operators are considered.
Our PLS-Completeness results shed light on the worst case behavior that
can be expected of an MA that belongs to the classes of algorithms
analyzed.
We also mention some connections between the Polynomial Local
Search Complexity theory and Kolmogorov Complexity theory in the context
of evolutionary algorithms understanding.
We show that the set-theoretic semantics for $\lambda^{\to2}$ is
complete by inverting evaluation using decision trees. This leads
to an implementation of normalisation by evaluation which is
witnessed by the source of our paper being a literate Haskell
script. We show the correctness of our implementation using logical
relations.
Functional Reactive Programming (FRP) is a conceptual framework for
programming reactive systems using ideas from functional programming.
Yampa is the latest Yale implementation of FRP. It differs from earlier
FRP implementations in several ways. The most obvious is perhaps that it
is structured using arrows, giving Yampa programs a distict syntactic
feel compared to its predecessors. However, more important is that Yampa
provides constructs for programming systems with highly dynamic
interconnection structure. Our experience with Yampa thus far also
indicates that it is much less prone to performance problems like space
leaks than previous FRP systems. This talk gives an overview of Yampa,
illustrating with concrete examples. Particular emphasis is placed
on the constructs for programming systems with dynamic structure.
Fokkinga (1994) constructed an adjunction between the category of
F-algebras and the category of lifted F-algebras for monads M given a
certain natural transformation dist_F, and regular F. The left
adjoint in the construction (with its preservation of colimits) allow
translation of recursion schemas to schemas parameterised by monads.
In this talk I will explain Fokkinga's construction and give concrete
examples of its use in functional programming, e.g. the relationship
between recursion and stateful objects represented by state monads.
I further discuss shortcomings with Fokkinga's monadic lifting, and
describe my current work on generalising the lifting construction.
The aims of this talk are to introduce quantum computers, how they work, and
fully explain some example algorithms that outperform classical computations.
Postscript of the paper can be found here.
Slides of the talk:
School of Computer Science and IT
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB
United Kingdom