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 wrote:
>
> In hardware, most devices are parameterised by
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 ezt írta (időpont: 2019. ápr. 30., K
15:28):
> In hardware, most
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
