Most hardware verification seems to be done in some variant of HOL, and its 
type system is too poor for dependent type theory (and even for type 
Freek Wiedijk: "The HOL type system is too poor. As we already argued in the 
previous section, it is too weak to properly do abstract algebra." [Wiedijk, 
2007, p. 130]
See also:

Tom Melham's Extended HOL provides quantification over types, but no type 
abstraction and no dependent types.
HOL2P and HOL-Omega do have type abstraction, but do not provide full dependent 
types (if I'm not mistaken):

For full dependent type theory substitution at the type level is required.
I had implemented this at some stage in the development of R0, but removed it 
later since it seemed too experimental then:
        "[O]ne would like to infer from fuv(2):vectype(2) to fuv(2):R^2. An 
implementation of a substitution rule directly at the type (subscript) level 
appeared too experimental to the author and was removed, since further case 
studies (here using the recursion operator R) should be undertaken."
Plus, the efforts for formalizing the proofs in a Hilbert-style system for the 
recursion operator R necessary for number theory were too large:
        "As shown further below [pp. 388 ff.], the recursion operator R 
[Andrews, 2002, pp. 281 f., 284] can be used to define a function which obtains 
the type of a vector of a given dimension."

One option might be implementing a natural deduction variant of R0 (with 
substitution at the type level) in a logical framework such as Isabelle or 
Cris Perdue has implemented a natural deduction variant of Q0:
Since Q0 and R0 use the description operator, one would also get rid of the 
epsilon operator in HOL and the implicit Axiom of Choice (the use of which 
then, as desired, would become explicit).
Mike Gordon: "It must be admitted that the ε-operator looks rather suspicious." 
[Gordon, 2001, p. 24] "The inclusion of ε-terms into HOL 'builds in' the Axiom 
of Choice [...]." [Gordon, 2001, p. 24]

Kind regards,

Ken Kubota


Ken Kubota

> Am 30.04.2019 um 15:28 schrieb Lawrence Paulson <>:
> In hardware, most devices are parameterised by a numerical bit width: buses, 
> counters, adders, registers, etc. So it seems obvious that people might have 
> tried to perform hardware verification using some form of dependent type 
> theory. Are there any particularly notable achievements along those lines? 
> And if not, why not?
> Larry Paulson

hol-info mailing list

Reply via email to