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