I don't know if this is notable: https://dspace.library.uu.nl/handle/1874/298576
An there is Kami from Chlipala et al that uses Coq, I don't know it in detail whether they really use dependent types. - Gergely Lawrence Paulson <[email protected]> ezt írta (időpont: 2019. ápr. 30., K 15:28): > 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 >
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
