John Herbert
3 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.
John Herbert
John Herbert, University of Cambridge Computer Laboratory and later SRI's Cambridge office. Three records, and they are the corpus's clearest evidence that the Cambridge HOL work was applied to hardware somebody actually built and shipped, rather than only to teaching examples.
**The chip, twice.** gordon1985formal, TR-66 of 1985, is a formal hardware verification methodology "and its application to a network interface chip", with Gordon. herbert1988case, TR-123 of 1988, is Herbert alone on the Cambridge Fast Ring ECL chip. The Fast Ring was the Computer Laboratory's own local-area network, so the device being verified was a component of the department's working infrastructure -- not a counter, not a toy ALU, not Gordon's computer. Almost everything else in the corpus's 1980s Cambridge cluster proves something about an example chosen to be provable. These two prove something about a part that had to work.
**The other side of the verification/description gap.** boulton1990hol, TR-199 of 1990, with Boulton, Gordon and Van Tassel, verifies designs written in ELLA rather than designs written in HOL. That places Herbert on both halves of the problem the corpus watches: proving things about real devices, and meeting the notations engineers use instead of asking them to change. boulton1992hol, the ELLA semantics underneath it, is held as a citation only.
**A note on reading these.** Both Cambridge reports here are scan-only -- 61 and 67 words respectively from text extraction, over 42 and 39 leaves -- so they answer no text search and must be read by rendering pages. That is a property of the copies, not of the work, and it is why two of this corpus's more interesting industrial applications are among its least visible holdings.