Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Ascii module

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ascii module


chronological Thread 
  • From: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
  • To: Frederic Blanqui <frederic.blanqui AT inria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Ascii module
  • Date: Fri, 4 Mar 2011 10:30:04 +0100

Thank you for the references, this work of yours looks quite interesting 
indeed.

Stéphane

On Thu, Mar 3, 2011 at 10:39 AM, Frederic Blanqui
<frederic.blanqui AT inria.fr>
 wrote:
> 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.
>>>
>>
>>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06




Archive powered by MhonArc 2.6.16.

Top of Page