I was wondering if anyone has verified the CAN or controller area network using ISABELLE ?? David
--- On Mon, 4/30/12, [email protected] <[email protected]> wrote: From: [email protected] <[email protected]> Subject: isabelle-dev Digest, Vol 59, Issue 52 To: [email protected] Date: Monday, April 30, 2012, 6:00 AM Send isabelle-dev mailing list submissions to [email protected] 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 [email protected] You can reach the person managing the list at [email protected] 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 <[email protected]> To: DEV Isabelle Mailinglist <[email protected]> Subject: [isabelle-dev] Alternative approach to ?efficient? natural numbers Message-ID: <[email protected]> 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 <[email protected]> To: [email protected] Subject: Re: [isabelle-dev] Isabelle release test website Message-ID: <alpine.lnx.2.00.1204291629510.19...@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 <[email protected]> To: [email protected] Subject: [isabelle-dev] Haskabelle update? Message-ID: <alpine.lnx.2.00.1204291650040.19...@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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev End of isabelle-dev Digest, Vol 59, Issue 52 ********************************************
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
