STEPHEN BROOKES
Associate Professor, Computer Science

My main interests concern the mathematical semantics of programming languages. I believe that proper attention to semantic foundations can yield significant benefits in developing techniques for proving properties of programs, in program design, in language design and implementation.

I am particularly interested in developing intensional semantic models, in which one is able to reason both about the correctness and efficiency of programs. This is in contrast to most traditional semantic models, which are extensional and focus on the input-output behavior of programs while abstracting away from computation strategy. I am working mainly on the semantic foundations of parallelism. This work includes the development of axiomatic proof techniques for establishing behavioral properties of parallel systems, design rules for parallel networks that guarantee desirable behavior such as deadlock-freedom, and the design and implementation of programming languages that employ parallelism uniformly and cleanly.

A semantics for a programming language is an assignment of meanings to program terms. For a semantics to be useful it should accurately capture the computational behavior of program terms, at an appropriate level of abstraction.

I believe that major improvements in the formal treatment of program properties can be achieved by paying careful attention to semantics. If we want to reason about a particular behavioral notion (such as partial correctness) we should first define a mathematical model for programs which precisely captures this behavior without being overly complicated. Ideally, we would like a fully abstract semantics: terms should be given the same meaning precisely when the terms would induce identical behavior in all program contexts. The construction of fully abstract models is by no means an easy task, and depends in any case on the underlying notion of behavior.

For modelling and reasoning about certain types of program behavior, such as partial or total correctness, an extensional semantics is satisfactory: the meaning of a program can be chosen to be a (partial) function from initial states to final states, and all details of how the program goes about its computation can be suppressed since all we really need to keep track of is the state transformation that the program induces. However, such a semantics is no use if we want to make comparisons between programs for the same function. In an extensional semantics all sorting programs have the same meaning, whereas we might well want to design a semantics with which we can compare sorting programs with different computation strategies. This motivation leads to a desire for a theory of intensional semantics. In an intensional semantics the meaning of a program is taken to be an algorithm rather than simply a function. An algorithm can be viewed as a function together with a (mathematical representation of a) computation strategy. I have recently developed a category-theoretic approach to the modelling of algorithms, and applied these ideas to the semantics of the lambda calculus. In the resulting semantic model, there is a complete partial order on algorithms and standard operations such as composition, application, and currying are continuous; thus, one may define algorithms recursively and use the standard techniques of denotational semantics (least fixed points) to reason about recursive programs, even at this intensional level. This approach using categories is rather general, and I am exploring several other possible applications.

Semantic principles and insights should be used in the design of new programming languages, to avoid the development of cumbersome languages in which the programmer may have to labor to overcome the syntactic quirks and idiosyncrasies of the programming language in order to express his algorithm as a program. I am particularly interested in designing a language that embodies parallelism uniformly: it ought to be as easy to specify parallel expression evaluation as it is to specify parallel execution of statements, and it ought to be easy to put together the results of parallel activities. The choice of an appropriate set of primitives for such a language should be guided by proper attention to semantic foundations, and I am carrying out research on this topic.