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 <l...@cam.ac.uk> 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
> 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

Reply via email to