[Hol-info] [Deadline Extension] Formal Verification of Physical Systems (FVPS 2019)

= 2nd Workshop on Formal Verification of Physical Systems (FVPS 2019) Colocated with CICM 2019 July 8, 2019

Re: [Hol-info] hardware verification and dependent types

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