Preface

Summary

This book is based on material presented at a summer school on Semantics and Logics of Computation that took place at the Isaac Newton Institute for Mathematical Sciences, Cambridge UK, in September 1995. The school was sponsored by the EU ESPRIT Basic Research Action on Categorical Logic in Computer Science (CLiCS I & II) and aimed to present some modern developments in semantics and logics of computation in a series of graduate-level lectures. Most of the material presented here has not previously been accessible in such a coherent and digestible form. This Preface gives a thematic overview of the contents of the book. It also briefly sketches the history of the two CLiCS projects which came to an end with the summer school.

Games, proofs and programs One of the most exciting recent developments in programming semantics has been the use of games and strategies to provide a more fine grained semantics than that provided by domain-theoretic models. This ‘intensional semantics’ aims to combine the good mathematical and structural properties of traditional denotational semantics with the ability to capture dynamical and interactive aspects of computation, and to embody the computational intuitions of operational semantics. More pragmatically, game semantics have been used to solve long-standing ‘full abstraction’ problems for PCF (a simple language for Programming Computable arithmetic Functions of higher type) and Idealised Algol. In other words games have provided syntax-independent models of these languages which precisely capture the operationally defined notion of ‘contextual equivalence’ of program expressions.