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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
