This doesn’t directly answer the question, but the Sail project (https://www.cl.cam.ac.uk/~pes20/sail/) designed a relatively lightweight dependent type mechanism for describing ISAs.
Scott > On 2019/04/30, at 14:28, Lawrence Paulson <l...@cam.ac.uk> wrote: > > 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 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
