See project bibliography.
Abstract. What does it mean for a piece of software to be correct? There are many possible degrees and dimensions of correctness, e.g. safety, functional correctness, computational complexity, and security. To grapple with this diversity of verification requirements, semanticists develop mathematical models of program behavior that put into relief different aspects of the physical reality of program execution on hardware, just as physicists create many idealized mathematical models to study different aspects of the material reality of the universe.
Mathematical models enable us to reason about program behavior by viewing highly complex objects as being glued together from smaller, simpler objects that are easier to study in isolation. For instance, operational models aim to reduce the behavior of a process to that of individual steps of discrete computation that take place on an idealized computer; in contrast, denotational models reduce the complex global behavior of a process to the simpler local behavior of its constituent subroutines. One advantage of operational methods is that they are applicable even in situations that challenge the modularity of denotational semantics, e.g. where it is not yet understood how to reduce the global behavior of a program to that of its components. On the other hand, denotational methods provide vastly stronger and simpler reasoning principles for program verification when available.
The central thesis of denotational semantics is that programs arrange themselves into geometrical spaces called computational domains, and that a computational process can be thought of as the limit of a sequence of continuous transformations on these domains. Although this thesis has been amply born out for simple kinds of program, today’s most urgent verification requirements pertain to program constructs like concurrency and side effects whose treatment requires the introduction of new kinds of space: for instance, the correct treatment of branching behavior for concurrent processes requires the introduction of higher-dimensional computational domains in which programs can “remember” the specific way that they were glued together.
This project will extend the reach of denotational semantics and its attendant advantages for program verification into terrains where scientists have historically struggled to enact the reduction of global behavior to local behavior, making essential use of new advances in the homotopical and geometrical understanding of computation via higher dimensional category theory and topos theory. I will investigate two areas that are ripe for reaping the benefits of a modern denotational semantics: the semantics of side-effects which govern the interaction of a program with the computer’s memory, and the semantics of concurrent processes.