Principles of Programming
Overview
This group investigates the semantics and formal methods for programming languages with imperative features, either alone or combined with functional and object-oriented features. Below are some of our research areas; as you can see, they overlap to a large extent.
Main Academic Staff:
Dan Ghica
Paul Levy
Uday Reddy
Eike Ritter
Alan Sexton
Hayo Thielecke
PhD Students:
Mr Chris Ross
State manipulation
Common programming facilities, such as generating new storage cells, and allowing storage cells to store other storage cells (pointer structures, in other words) pose some surprising problems both for modelling and for reasoning. Work addressing these questions has been done by Reddy in Idealized Algol and by Levy in call-by-push-value, but many questions remain open, particularly about parametricity for the more recent models.
Types and effect systems
Types and effects can express that a program will behave in a disciplined way. Moreover, they do so statically, that is, before the program is run, and could be checked automatically by the compiler. Type safety in particular has recieved a great deal of attention in connection with Java. For a sophisticated language that combines functions or objects with computational effects, a type system alone may not be expressive enough; a type and effect system enhances an underlying type system with effect information. Thielecke's recent work uses types and effects for control. Many control constructs, such as exceptions, have been shown to be of a stylized form by using a linear type system for continuation passing. In related work, an effect system for control is mapped to polymorphically typed continuation passing. Future work will study type and effect system for computational effects in general, and pointers in particular.
Call-by-push-value
Much work about languages combining imperative and functional features has focussed on either call-by-name (CBN) or call-by-value (CBV) languages. Building on work of Moggi, Filinski and others, Levy analyzed a wide range of CBN and CBV semantics and noticed a pattern: it emerged that a single fine-grain language, called "call-by-push-value" (CBPV), underlies both of the older paradigms, and so the constructs of CBV and CBN can be seen as particular idioms in CBPV. Examples of models with CBPV structure include domains, possible worlds, continuations and games, and even more models are currently emerging (e.g. lower powerdomain).
Subsequent work has extended CBPV with constructs for the stacks that arise during execution, and used these to show that the algebraic concept of adjunction accurately characterizes CBPV models.
Game semantics
In the past decade game semantics has emerged as a new and successful paradigm in the field of semantics of logics and programming languages. Game semantics made its breakthrough in computer science in the early 90s, providing an innovative set of methods and techniques for the analysis of logical systems. Subsequently, game-semantic techniques led to the development of the first syntax-independent fully-abstract models for a variety of programming languages, ranging from the purely functional to languages with non-functional features such as control, references or concurrency. Ghica and McCusker, followed by Abramsky, Murawski, Ong and others, developed an algorithmic approach to game semantics with a view to applications in computer assisted program verification.