Re: [isabelle] Word32/64 ?



On Wed, 27 Jan 2010, Rafal Kolanski wrote:

One approach for high-performance code seems to be going in reverse, i.e. parsing annotated SML/C/Haskell/whatever into Isabelle, where you can pick your own translation, but have to pay by having to specify the semantics also.

BTW, "high-performance" in SML (as implemented in Poly/ML) means to use the default int, i.e. the proper mathematical (unbounded) integers, not machine words. Poly/ML optimizes the representation of values for the demands of symbolic computation, not for bare metal operations. So proper ints, lists (cons cells), datatypes are fast, but Word32 is really slow.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.