Jeffrey J. Joyce
A grouping.
Jeffrey J. Joyce, at the Cambridge Computer Laboratory in Mike Gordon's HOL group alongside Avra Cohn. Two records, three years apart, and together they show one instinct applied at two scales.
In 1987 he gives MOS devices a four-valued semantics -- Lo, Hi, Zz for high impedance, Er for error -- and then writes down an explicit abstraction function into boolean logic, using Hilbert's choice operator so that the values the abstraction does not cover are fixed but unknown. The partiality of the model is thereby enforced by the logic: nothing can be proved by appealing to what an undriven wire abstracts to. In 1990 the same instinct reappears as generic specification, whose stated purpose is "a sharp distinction between what has and what has not been formally considered in a proof of correctness", now applied to whole system layers rather than to signal values. Read the pair in order and the dissertation is the earlier idea generalised.
That makes him the constructive counterpart to Cohn. She argues that a verification relates models to each other by a relation that cannot be checked; he keeps building machinery whose point is to make the edge of the model visible inside the formalism. Neither position refutes the other and the corpus holds both.
What is still missing is the work each of them is best known for outside this corpus: the Tamarack microprocessor proof, which Cohn singles out because it reached the transistor level on a chip that was actually fabricated. It is not in either record held here. The likeliest home is UCAM-CL-TR-100, "Proving a computer correct in higher order logic" (Joyce, Birtwistle and Gordon, December 1986), on the same open series; the intervening reports TR-136, TR-147, TR-167 and TR-178 are also unfetched and are listed in the note on the 1987 report.