Publications

My publications are available from the Computer Science department publications repository.

Research Interests

Research Interests

My research interests are in the fields of functional programming and hardware verification.

Functional programming

I am presently interested in exploring the use of highly interactive visual interfaces to Haskell as a means of allowing non-technical users to benefit from the expressiveness, clarity and security that contemporary functional programming languages offer. The main thrust of the research is in devising ways of graphically presenting the various data structures in a program in a way that allows a user to specify their "look and feel" in an easy and intuitively natural way. One way in which this is being done is by allowing the variables in a program to be be annotated with "styles" drawn from a stylesheet. Another aspect of the research is in devising ways that allow any changes a user may make to the graphical representation of a datastructure to be immediately reflected in the source text of the program. This will enable a user (whose interest and expertise may be in a domain far removed from computing) to develop powerful, secure programs in an incremental, exploratory fashion.

The VITAL project

These principles are presently being put into practice in the VITAL project (Visual Interactive Typed Applicative Language). A proof of concept implementation has been completed and work is presently underway on a full implementation.

The PIVOTAL project

This project has similar aims to the Vital project but, unlike Vital, this one is implemented entirely in Haskell.

Hardware verification

I have long taken an interest in how various kinds of higher-order logic can be used as a natural form of specification language for describing the structure and behaviour of digital systems and for reasoning about their interrelationship. Some of my work has been in studying how a so-called dependently-typed logic (in effect, a strongly-typed logic in which the types can be treated as values) can be used for reasoning about very general classes of digital designs. A particular result that I established demonstrated how the behavioural properties of an entire class of digital designs (arithmetic systems implemented iteratively in time or space) can be captured by a single, highly-parameterised theorem (the Factorisation Theorem).

More recently, I have been exploring the use of higher-order logic to specify and reason about the digital systems implemented not in terms of conventional logic gates but, rather, at the level of individual electronic devices (transistors, resistors, etc.). This is of particular interest since, in practice, many digital systems tend to be implemented at this lower level of abstraction, and there is an urgent need for formalisms that will allow the intended behaviour of such systems to be described and particular implementations to be formally verified.

Postgraduates

I would be interested in hearing from potential research students interested in working in fields related to functional programming and visualisation techniques. Current areas of interest include creating new paradigms for visualisation and interaction and interactive type checking (please see TCS project list for details).