This project seeks to develop denotational semantics for a variety of programming languages, tailored to support compositional reasoning about various important forms of program behavior. It studies a typical functional programming language, and two typical parallel imperative languages: a language for shared-variable parallelism, and a language of communicating processes related to Hoare's CSP and Milner's CCS. Notions of behavior considered for the parallel languages include safety and liveness properties, and partial and total correctness, assuming various forms of fairness properties that correspond to natural assumptions about the runtime execution of concurrent processes. This should permit reasoning about parallel programs to be carried out without knowledge of or reference to details concerning scheduling. There also is a research focus on intensional properties concerning runtime and efficient use of resources. Technically, the project aims to develop fully abstract semantics, with respect to a variety of important notions of program behavior. A semantics is fully abstract if it gives the same meaning to two program phrases precisely when they induce identical behavior in all program contexts. This provides a rigorous criterion for judging the utility of a semantics in supporting compositional or modular reasoning about program behavior. The long term goal is the development of a unifying framework suitable for establishing and exploiting relationships between languages, models, and proof methods for reasoning about programs. In particular, the research seeks to establish a mathematically tractable theory and use it to develop practical techniques for modular design and analysis of parallel programs.
