Understanding Z : A specification language and its formal semantics. - J. Michael Spivey (1985)

Laws of Programming. - C. A. R. Hoare; Ian J. Hayes; Jifeng He 001; Carroll Morgan; A. W. Roscoe 001; Jeff W. Sanders; Ib Holm Sørensen; J. Michael Spivey; Bernard Sufrin (Commun. ACM, 1987)

Understanding Z - a specification language and its formal semantics (reprint). - John Michael Spivey (Cambridge University Press, 1989)

The Z notation - a reference manual. - John Michael Spivey (Prentice Hall, 1989)

A Categorial Approch to the Theory of Lists. - J. Michael Spivey (MPC, 1989)

An introduction to Z and formal specifications. - J. Michael Spivey (Softw. Eng. J., 1989)

Type Inference in Z. - J. Michael Spivey; Bernard Sufrin (VDM Europe, 1990)

A Functional Theory of Exceptions. - J. Michael Spivey (Sci. Comput. Program., 1990)

Specifying a Real-Time Kernel. - J. Michael Spivey (IEEE Softw., 1990)

Z Notation - a reference manual (2. ed.). - J. Michael Spivey (Prentice Hall, 1992)

Unification: A Case-Study in Data Refinement. - J. Michael Spivey (Formal Aspects Comput., 1995)

An introduction to logic programming through Prolog. - J. Michael Spivey (Prentice Hall, 1996)

The Consistency Theorem for Free Type Definitions in Z. - J. Michael Spivey (Formal Aspects Comput., 1996)

Richer Types for Z. - J. Michael Spivey (Formal Aspects Comput., 1996)

Algebra of Logic Programming. - Silvija Seres; J. Michael Spivey; C. A. R. Hoare (ICLP, 1999)

Higher-order transformation of logic programs. - Silvija Seres; J. Michael Spivey (LOPSTR, 2000)

Meeting the Challenge of Object-Oriented Programming. - J. Michael Spivey (ZB, 2000)

Combinators for breadth-first search. - J. Michael Spivey (J. Funct. Program., 2000)

Functional Reading of Logic Programs. - Silvija Seres; J. Michael Spivey (J. Univers. Comput. Sci., 2000)

Fast, accurate call graph profiling. - J. Michael Spivey (Softw. Pract. Exp., 2004)

On Barron and Strachey's cartesian product function. - Olivier Danvy; J. Michael Spivey (ICFP, 2007)

Algebras for combinatorial search. - J. Michael Spivey (J. Funct. Program., 2009)

When Maybe is not good enough. - J. Michael Spivey (J. Funct. Program., 2012)

Faster coroutine pipelines. - J. Michael Spivey (Proc. ACM Program. Lang., 2017)