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
abstraction).
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]
http://www.owlofminerva.net/files/fom.pdf#page=10
See also:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-April/msg00102.html
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):
http://www.owlofminerva.net/files/fom.pdf#page=1
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."
http://www.owlofminerva.net/files/formulae.pdf#page=12
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."
http://www.owlofminerva.net/files/formulae.pdf#page=12
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
Metamath.
Cris Perdue has implemented a natural deduction variant of Q0:
http://prooftoys.org
http://mathtoys.org
http://www.owlofminerva.net/files/fom.pdf#page=2
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]
http://www.owlofminerva.net/files/fom.pdf#page=9
Kind regards,
Ken Kubota
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100
> Am 30.04.2019 um 15:28 schrieb Lawrence Paulson <[email protected]>:
>
> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
