Joseph Morris's interest is in constructing high-quality computer software, especially software in which users can have a very high confidence that it performs according to specification. More particularly, Prof. Morris is interested in developing mathematical methods of reasoning about programs, and in using mathematics to extract guaranteed correct programs from formal specifications. His areas of expertise include formal logic, theories of nondeterminacy, concurrency, specification and programming languages, program verification, formal semantics, and effective reasoning about all aspects of developing computer software.

Prof. Morris's primary theoretical interests at present are many-valued logics and theories of nondeterminacy. Nondeterminacy is a crucial component of specification languages, but it remains to discover how best to reason about it. Prof. Morris has designed a family of many-valued logics with the specific aim of supporting reasoning about nondeterminacy. He is exploring ways in which nondeterminacy can facilitate proofs of program correctness, in particular programs that employ data refinement in their construction.

Prof. Morris is developing a comprehensive deductive calculus of programming supports both imperative and functional programming. At the core of the calculus is a typed higher-order four-valued logic, the extra values catering for nondeterminacy and partiality. The goal is to deliver a calculus that is hugely richer than the refinement calculus, has a surer basis in logic, is provably consistent, and leads to innovative ways of reasoning about programming whether applied formally or not. Most recently, he has begun working on calculi for developing reliable object-oriented programs including the use of machine verification. His research is supported by grants from Enterprise Ireland and Science Foundation Ireland.