beaneater.org.uk Nicholas Wolverson scribbles on his screen

Research

Budapest


01 April 2008
(15:33)

Hi from Budapest.

Danube from Margitsziget ? Conference Venue

I'm here for the ETAPS conference, or specifically to give a talk at the GaLoP workshop. Here until Monday...

Comment | Permalink | in categories Log Travel Research  
colin

Impressive. Good luck.

michael eng

have dobos torta at gerbeaud haz. the locals will tell you it's the best in the world, they could be right?

Declaration of intent


29 October 2007
(08:58)

On Friday I made a declaration of intent to submit my thesis. This has to happen two months before submission, and involves signing some forms and giving an Abstract. Here it is:

Game semantics for object-oriented languages

This thesis investigates the relationship between object-oriented programming languages and game models of computation. These are intuitively well matched: an object encapsulates some internal state and presents some behaviour to the world via its publicly visible methods, while a strategy for some game represents the possible interactions of a program with its environment.

We work with a simple and well-understood game model. Rather than tailoring our model to match some existing programming language, we view the simplicity of our semantic setting as a virtue, and try to find the appropriate language corresponding to the model.

We define a class-based, stateful object-oriented language, and give a heap-based operational semantics and an interpretation in our game model. At the heart of this interpretation lies a novel semantic treatment of the phenomenon of data abstraction. The model closely guides the design of our language, which enjoys an intermediate level of expressivity between that of first-order and general higher-order store.

The agreement between the operational and game interpretations is verified by a soundness proof. This involves the development of specialised techniques and a detailed analysis of the relationship between the concrete and abstract views. We also show that definability and full abstraction hold at certain types of arbitrary rank, but are problematic at other types.

We conclude by briefly discussing an extended language with a control operator, along with other extensions leading to a possible core for a more realistic programming language.

Comment | Permalink | in categories Log Uni Research modified 29 October 2007 (22:26) 
colin

What a fine declaration. You always did say I wouldn't understand what you were doing, and you were right as usual.

My research


03 December 2004
(15:58)

I don't think I've ever really explained what I'm doing my Ph.D. on, in laymans terms. Let's try; please have patience and excuse the length, but it is hard to write accurately but non-technically. I assume you know that computers run programs written by fallible humans.

I am working towards an object-oriented programming language based on game semantics.

Semantics

Let's start with semantics. When I say "semantics" I mean "programming language semantics"; given a computer program, what is its meaning? The aim here is to give an formal definition which unambiguously assigns a meaning to every program one could write in some programming language. This is in contrast to the "traditional" methodology of writing stacks of unreadable technical prose, or the more ad-hoc method of defining the meaning of programs by what a particular computer (and compiler, operating system, etc.) actually does with them.

There are a multitude of ways of doing this, and I shall describe two broad camps. One can give a set of rules specifying how the state of some (hypothetical) computer should behave in order to run your program (Operational Semantics). Alternatively, one can give a mathematical account of semantics, where the meaning of programs are given in some mathematical structure (Denotational Sematics).

Diving straight into that second idea, we can think of a computer program as something that takes some inputs and gives some outputs. The bells and whistles of modern graphical environments may obscure this notion, but fundamentally you are supplying input to a program somehow, and it is giving you some feedback. One can think of this as a mathematical function from inputs to outputs, and this is the basis for much work in denotational semantics. Of course in actual fact things are not so simple, but there is a great deal of work in considering program semantics in the setting where data is represented by some structured sets, and computation is represented by structure-preserving functions between these (this is the essence of Domain Theory, as I see it).

Game Semantics

Okay, now we get to Game Semantics. When I say "game" I am thinking of a two-player game, where each party plays alternately, such as in Chess. There is some set of moves one can make, and in particular at each position throughout a play of the game, there will be some moves that one is allowed to make. A strategy for such a game is just a sort of formalisation of the thinking of a player~imagine that, before starting to play, you have decided how to play at any given position of the board (the practicality of this is not an issue for us).

The words Game Theory may be familiar to you, but are not entirely relevant to game semantics. Typically in game theory one talks about players choosing strategies in order to maximise some outcome (get rich or whatever), possibly involving some "dice-rolling" in the process. The games I'm talking about do not have a notion of winning or losing; that's not what they're for.

Instead of thinking of a computer program as some function on structured sets, one can think of it as a strategy for some particular two-player game. I find this hard to explain, so let me give an example. Imagine that the program in question is the suitably simple "doubling" program: given some number as input, it will give twice that number as output. Okay, we could just think of it as a function on the natural numbers, but bear with me. I want to know the result of the program, so I ask the program "what is your value?". The program responds by asking me the value of the input; I proceed to say that the input is 21. The program then replies that the answer is 42.

It is impossible to decide the worth of game semantics on such a trivial example. The field has had some successes, but is probably not the answer to life, the universe and everything. In any case, there are particular types of games and constructions on games which we have been investigating (and now we're finally getting to what I'm actually doing). I have a developing picture of some mathematical structures, which will hopefully support some particular programming language, which will be designed to exploit those structures.

Object-oriented Programming

Okay, here's the other half. I mentioned an object-oriented programming language. Perhaps this is less important, and this may not be what I want in the end, but we will stick with this for now. The fundamental thing in an object-oriented programming language is, funnily enough, the object. Based upon the real-world analogy of objects which interact with each other in various ways, we view a program as composed of a bunch of objects, where each object may consist of some data (for example the entry for a person in a telephone directory) and some ways to interact with that data (continuing the example, one could ask for the number of a particular person, or update their address).

My Research

I don't think the OOP paradigm has a great particular worth, but it is currently popular, and no doubt attempting to address some of the nicer and more familiar features in a principled way is a good idea. It seems that one could create a reasonable language with object-oriented and functional parts based on the aforementioned games, and it would be nice if that was an outcome of this research. Crucially, I am not trying to design a realistic programming language; my research is all about some semantic ideas, and any language which emerges will be a way of investigating those ideas rather than an end in itself.

Maybe next week we'll talk about Category Theory.

Comment | Permalink | in categories Log Uni Research modified 03 December 2004 (16:26) 
Helen

Yes!

Thankyou! you have done what i've been wanting you to do/say for ages. i.e. what your mind is into re reserch. So now I will read this at my leasure and I can let you get on with it/ or maybe even ask more! yet again from the masses who may not have had clear objectives, good info, Helen X