Prof Joe Morris

Name:Prof Joe Morris
Phone Number8419
E-Mail Address:
Work Area:Professor
HomepagePersonal Homepage

Selected Peer Reviewed Journals

  • J. Morris, A. Bunkenburg. 1998. Partiality and Nondeterminacy in Program Proofs. Formal Aspects Of Computing, 10,, pp76-96.
  • Joseph Morris. 1997. Non-Deterministic Expressions and Predicate Transformers. Information Processing Letters, 61, 5, pp241-246.
  • Joseph Morris. 1990. Programming by Expression Refinement: a Sequence of Examples. 11, 4, pp189-198.
  • Joseph Morris. 1989. Well-founded induction and the invariance theorem for loops. Information Processing Letters, 32,, pp155-158.
  • Joseph Morris. 1987. Varieties of Weakest Liberal Preconditions. Information Processing Letters, 25, 3, pp207-210.
  • Joseph Morris. 1985. The impact of computer science on mathematics in the engineering curriculum. International Journal Of Mathematical Education In Science And Technology, 16, 3
  • Joseph Morris. 1980. A starvation-free solution to the mutual exclusion problem. Information Processing Letters, 8, 2, pp76-80.
  • Joseph Morris. 1980. Traversing binary trees simply and cheaply. Information Processing Letters, 9, 5, pp197-200.

Selected Books

  • J.M. Morris, B. Aziz, F. Oehl. 6th International Workshop on Formal Methods, British Computer Society, 2003.
  • J. Morris, R. Shaw. 4th BCS FACS Refinement Workshop, Springer Verlag, Workshops in Computing,, 1991.

Selected Chapters

  • J.M. Morris. 1990. Programming by expression refinement: the KMP algorithm. Beauty is our Business, Springer Verlag,
  • J.M. Morris. 1981. A proof of the Schorr-Waite algorithm. Theoretical Foundations of Programming Methodology, Reidel Publishing,
  • J.M. Morris. 1981. A General Axiom of assignment. Theoretical Foundations of Programming Methodology, Reidel Publishing,
  • J.M. Morris. 1981. Assignment and linked data structures. Theoretical Foundations of Programming Methodology, Reidel Publishing,


  • J.M. Morris, Plug-and-play nondeterminacy, B 2007: Formal Specification and Development in B, 01-JAN-07 - 31-DEC-07, , 289 - 292
  • J.M. Morris & M. Tyrrell, Models for Higher-Order Nondeterministic Functions, 23rd British Colloquium for Theoretical Computer Science, 01-JAN-07 - 31-DEC-07,
  • M. Tyrrell, J.M. Morris, A. Butterfield, A. Hughes, A Lattice-Theoretic Model for an Algebra of Communicating Sequential Processes, 3rd International Colloquium on Theoretical Aspects of Computing, 01-JAN-06 - 31-DEC-06, , 123 - 137
  • M. Tyrrell, J.M. Morris, A. Butterfield, A. Hughes, Modelling unbounded demonic and angelic nondeterminacy for a process algebra, 4th Conf. on the Mathematical Foundations of Computer Science and Information Technology, 01-JAN-06 - 31-DEC-06, , 412 - 415
  • J.M. Morris, M. Tyrrell, A. Butterfield, Building a process algebra on a theory of refinement, Refinement Workshop, part of ICFEM 2005: 7th International Conference on Formal Engineering Methods University of Manchester, UK, 01-JAN-05 - 31-DEC-05,
  • G. Carter, R. Monahan, J.M. Morris, Software Refinement with Perfect Developer, 3rd IEEE Int. Conf. on Software Engineering and Formal Methods, 01-JAN-05 - 31-DEC-05, , 363 - 373
  • J.M. Morris, Augmenting Types with Unbounded Demonic and Angelic Nondeterminacy, Mathematics of Program Construction 2004, 01-JAN-04 - 31-DEC-04, , 274 - 288
  • A. Bunkenburg, J.M. Morris, Introduction to Expression Refinement, Glasgow Workshop on Functional Programming, 01-JAN-97 - 31-DEC-97,
  • J.M. Morris, S. Ahmed, Designing and refining specifications with modules, 3rd BCS FACS Refinement Workshop, 01-JAN-91 - 31-DEC-91,
  • S. Ahmed, J.M. Morris, Constructing and refining modules in a type theory, 4th BCS FACS Refinement Workshop, 01-JAN-91 - 31-DEC-91,
  • J.M. Morris & M. Schwartz, The design of a language-directed editor, ACM Symp. on Text Manipulation, 01-JAN-81 - 31-DEC-81, , 28 - 33