Joseph M. Morris and Malcolm Tyrrell
We prove that programs of a strict functional programming language behave as expected after the addition of unbounded demonic and angelic nondeterminacy. This technical report is not intended as a stand-alone work, but as a companion to a paper which explores how nondeterminacy gives rise to a theory of recursion.
J. Morris, M. Tyrrell, A. Butterfield, A. Hughes, W. Verbruggen
We establish the foundations of a lattice-theoretic model for a variant of communcating sequential processes. This technical report is not intended as a stand-alone work, but as a companion to a paper which defines the process algebra and describes its model. We give proofs for various theorems stated in that paper. In particular we prove that the axioms of the process algebra are sound.