[isabelle-dev] CAN CONTROLLER AREA NETWORK

[David Blubaugh]

I was wondering if anyone has verified the CAN or controller area network using ISABELLE  ??
 
David
 
 


--- On Mon, 4/30/12, isabelle-dev-request at mailbroy.informatik.tu-muenchen.de <isabelle-dev-request at mailbroy.informatik.tu-muenchen.de> wrote:


From: isabelle-dev-request at mailbroy.informatik.tu-muenchen.de <isabelle-dev-request at mailbroy.informatik.tu-muenchen.de>
Subject: isabelle-dev Digest, Vol 59, Issue 52
To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
Date: Monday, April 30, 2012, 6:00 AM


Send isabelle-dev mailing list submissions to
    isabelle-dev at mailbroy.informatik.tu-muenchen.de

To subscribe or unsubscribe via the World Wide Web, visit
    https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

or, via email, send a message with subject or body 'help' to
    isabelle-dev-request at mailbroy.informatik.tu-muenchen.de

You can reach the person managing the list at
    isabelle-dev-owner at mailbroy.informatik.tu-muenchen.de

When replying, please edit your Subject line so it is more specific
than "Re: Contents of isabelle-dev digest..."


Today's Topics:

   1. Alternative approach to ?efficient? natural numbers
      (Florian Haftmann)
   2. Re: Isabelle release test website (Makarius)
   3. Haskabelle update? (Makarius)


----------------------------------------------------------------------

Message: 1
Date: Sun, 29 Apr 2012 15:51:26 +0200
From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
To: DEV Isabelle Mailinglist <isabelle-dev at in.tum.de>
Subject: [isabelle-dev] Alternative approach to ?efficient? natural
    numbers
Message-ID: <4F9D475E.5030108 at informatik.tu-muenchen.de>
Content-Type: text/plain; charset="iso-8859-15"

Hi all,

I did an experiment with Flyspeck-Tame (on macbroyXY):

Using the Efficient_Nat theory where Isabelle nat is directly
represented as PolyML int:

> Finished HOL-Flyspeck-Tame (11:50:46 elapsed time, 13:54:35 cpu time, factor 1.17)

Using the Target_Numeral theory where Isabelle nat is an abstract
datatype over PolyML int:

> Finished HOL-Flyspeck-Tame (10:55:49 elapsed time, 13:57:31 cpu time, factor 1.27)

The reason why this has the same magnitude of runtime is that in PolyML
trivial datatypes like

> datatype nat = Nat of int
> fun int_of (Nat k) = k

are optimized away.

This is a proof of concept that it is possible in the future to have
just *one* type which is mapped onto target language numerals by
default, and to refine nat and/or int to use this is implementation if
desired, rather than adhoc code_const setups etc. for nat and int.  Cf.
also https://isabelle.in.tum.de/community/Numerals

Cheers,
    Florian

P.S. This his no consequences for the upcoming release.

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120429/b9c957c6/attachment-0001.asc>

------------------------------

Message: 2
Date: Sun, 29 Apr 2012 16:35:02 +0200 (CEST)
From: Makarius <makarius at sketis.net>
To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Isabelle release test website
Message-ID:
    <alpine.LNX.2.00.1204291629510.19214 at macbroy21.informatik.tu-muenchen.de>
    
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

This is probably the last update of the test website 
http://www4.in.tum.de/~wenzelm/test/website/ before official release 
candidates for Isabelle2012 will be announced (also on isabelle-users).

The current plan for the deadline for point 0 (the repository fork) is 
02-May-2012 -- I will announce it again to make sure that no changeset 
gets in the wrong place in the critical moment.

Afterwards any important amendments need to be sent as individual 
changesets to me via email.


    Makarius


------------------------------

Message: 3
Date: Sun, 29 Apr 2012 16:51:04 +0200 (CEST)
From: Makarius <makarius at sketis.net>
To: isabelle-dev at in.tum.de
Subject: [isabelle-dev] Haskabelle update?
Message-ID:
    <alpine.LNX.2.00.1204291650040.19709 at macbroy21.informatik.tu-muenchen.de>
    
Content-Type: TEXT/PLAIN; format=flowed; charset=US-ASCII

Who is maintaining Haskabelle?  Are there plans to update it for the 
coming release?

So far I have bundled Haskabelle2011-1.tar.gz from last time.


    Makarius


------------------------------

_______________________________________________
isabelle-dev mailing list
isabelle-dev at mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


End of isabelle-dev Digest, Vol 59, Issue 52
********************************************
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120430/0195646c/attachment.html>