Unifying theories of undefinedness in UTPJim Woodcock, University of York, UK.
In previous work, based on an original idea due to Saaltinck, we proposed a unifying theory of undefined expressions in logics used for formally specifying software systems. In our current paper, we instantiate these ideas in Hoare and He's Unifying Theories of Programming, with each different treatment of undefinedness formalsied as a UTP theory. In this setting, we show how to use classical logic to prove facts in a monotonic partial logic with guards, and we describe the guards for several different UTP theories. We show how classical logic can be used to prove semi-classical facts. We apply these ideas to the COMPASS Modelling Language (CML), which is an integration of VDM and CSP in the Circus tradition. We link CML, which uses McCarthy's left-to-right expression evaluation, to VDM, which uses Jones's three-valued Logic of Partial Functions, and to Circus, which uses a semi-classical logic.
Unifying Theories of Programming with MonadsJeremy Gibbons, University of Oxford, UK.
The combination of probabilistic and nondeterministic choice in program calculi is a notoriously tricky problem, and one with a long history. We present a simple functional programming approach to this challenge, based on algebraic theories of computational effects. We make use of the powerful abstraction facilities of modern functional languages, to introduce the choice operations as a little embedded domain-specific language rather than having to define a language extension; we rely on referential transparency, to justify straightforward equational reasoning about program behaviour.