X-IronPort-MID: 1747572217
X-SBRS: 4.2
X-BrightmailFiltered: true
X-Brightmail-Tracker: AAAAAA==
X-Ironport-AV: i="3.97,194,1125896400"; 
   d="scan'208"; a="1747572217:sNHT16380580"
Date: Mon, 10 Oct 2005 08:33:01 -0500
From: Jared Davis <jared@cs.utexas.edu>
User-Agent: Debian Thunderbird 1.0.2 (X11/20050602)
X-Accept-Language: en-us, en
To: ACL2 MTG List <acl2-mtg@lists.cc.utexas.edu>
Subject: This week in ACL2
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Reply-To: acl2-mtg@lists.cc.utexas.edu
Sender: owner-acl2-mtg@lists.cc.utexas.edu
X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
X-SpamAssassin-Status: No, hits=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-122 required=180

Hi,

At this week's ACL2 meeting I will talk about a fast implementation of records
for ACL2.  This library can be used to efficiently represent and simulate
fixed-size arrays and linear address spaces, e.g., processor memories, even
when such memories are very large (64-bits and beyond).

Despite its focus on efficiency, the library provides the same "hypothesis free
record theorems" as the ACL2 Records Library (misc/records), created by Rob
Sumners and Matt Kaufmann.  This library is discussed in the 2002 Workshop
paper, "Efficient Rewriting of Operations on Finite Data Structures in ACL2."

Hope to see you there,

     Jared