Strachey 100: an Oxford Computing Pioneer Oxford University

Types in programming languages are commonly thought of as a way of preventing certain bad things from happening, such as multiplying a number by a string. But this is only half of the benefit of types: it is what types are against. Types in programming languages are also what enable some good things to happen, such as selecting the right implementation of a heterogeneous operation like comparison or printing based on type information; this is what are types for. This ability is surprisingly powerful, and gives rise to a variety of highly expressive generic programming techniques. Jeremy illustrates with some examples based on the rank-polymorphic array operations introduced in Iverson’s APL: not only does the type information prevent array shape errors, it is what directs the lifting of operations across array dimensions.

In this presentation, Uday brings together two strands of Christopher Strachey’s thought: parametric polymorphism and abstract models of storage. The term parametric polymorphism was introduced in by Strachey who distinguished it from “ad hoc” polymorphism. In the words of John Reynolds, “a parametric polymorphic function is one that behaves the same way for all types,” whereas an ad hoc polymorphic function may have unrelated meanings at different types. A very similar intuition arose in mathematics, some twenty years earlier, for which Eilenberg and MacLane proposed a “General Theory of Natural Equivalences”, what we now call category theory. Relating the two notions allows us to develop a broad view of “parametricity” (the idea of acting the same way for all types), which
is applicable not only to programming languages but also to mathematics and perhaps other disciplines. A particularly important application of this broad view is for Strachey’s “mathematical semantics” of programming languages.

For modelling imperative programming languages that operate by manipulating a store, Strachey presented a basic model of storage based on “locations”, while promising a further paper on an “abstract model of storage” to appear in future. Unfortunately the latter never appeared. In succeeding work, Reynolds proposed an abstract model of store as well as an “intuitionistic” functor category approach to model the stack discipline of the store. O'Hearn and Tennent made the crucial observation that the model needs to be embellished with parametricity to capture the data abstraction aspects of the store.

In this talk, Uday reviews these developments as well as his own recent work on integrating the Reynolds model with parametricity to capture the fact that state changes of the store are irreversible. One way to understand these developments is to view them as a “parametric mathematical semantics” of programming languages.

Hongseok begins by talking about a program of Strachey’s that wrote “love letters” using the Manchester University computer. He then uses this as a lead in for discussing probabilistic methods of generating algorithms and programs.

Philip reviews Christopher Strachey’s influence on modern-day functional programming languages.

In this talk, Jane presents about her work on modelling dynamic behaviour of systems using quantative modelling techniques. Particular kinds of modelling diagrams are used and a mathematical approach to looking at their meaning is presented.

The logician Dana Scott played a crucial part in the story of denotational semantics, working for a term with Christopher Strachey in Autumn 1969, when he created a mathematical model for the foundation of the method. In this talk, Dana discusses this period as well as reminiscing about his life and career up to that point.