The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

You may be interested in knowing that, in the Formes team 
(http://formes.inria.fr/), we formalized in Coq a big part of the 
semantics of the ARMv6 processor. In fact, a big part of this 
formalization is generated automatically from the documentation. See 
http://www-rocq.inria.fr/~blanqui/rapido11-pdf.html for some details. A 
public release will certainly be done by the summer but I can provide 
some files if you are interested. We are also working on the processor 
SH4. Best regards, Frederic.

Le 03/03/2011 16:32, Stéphane Lescuyer a écrit :
> Incidentally, ARM processors were precisely the application I had in
> mind when I inquired about hundreds of constructors. That's why I'm
> curious about users who possibly tried that many constructors and
> their experience with it.
>
> S.
>
> On Thu, Mar 3, 2011 at 4:16 AM, Frederic Blanqui
> <frederic.blanqui AT inria.fr>
>   wrote:
> > I don't think that this is so uncommon. For instance, processors often have
> > dozens or hundreds of instructions. The ARMv6 processor has 147 32-bits
> > instructions and 73 16-bits instructions... Many term rewrite systems in the
> > Termination Problem Data Base have dozens of function symbols. Some have
> > more than several hundred symbols. So, I would say that hundreds of
> > constructors is not so uncommon. Now, thousands of constructors is perhaps
> > more uncommon. Frederic.