How Can I Do That with ACL2? Recent Enhancements to ACL2
The last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-event', 'mbe', and trust tags. In this paper we provide user-level summaries of some ACL2 enhancement...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2011-10-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1110.4673v1 |
id |
doaj-b6fde61f3af8411c9d41e858ced10bbb |
---|---|
record_format |
Article |
spelling |
doaj-b6fde61f3af8411c9d41e858ced10bbb2020-11-24T23:24:26ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-10-0170Proc. ACL2 2011466010.4204/EPTCS.70.4How Can I Do That with ACL2? Recent Enhancements to ACL2Matt KaufmannJ Strother MooreThe last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-event', 'mbe', and trust tags. In this paper we provide user-level summaries of some ACL2 enhancements introduced after the release of Version 3.5 (in May, 2009, at about the time of the 2009 ACL2 workshop) up through the release of Version 4.3 in July, 2011, roughly a couple of years later. Many of these features are not particularly well known yet, but most ACL2 users could take advantage of at least some of them. Some of the changes could affect existing proof efforts, such as a change that treats pairs of functions such as 'member' and 'member-equal' as the same function. http://arxiv.org/pdf/1110.4673v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Matt Kaufmann J Strother Moore |
spellingShingle |
Matt Kaufmann J Strother Moore How Can I Do That with ACL2? Recent Enhancements to ACL2 Electronic Proceedings in Theoretical Computer Science |
author_facet |
Matt Kaufmann J Strother Moore |
author_sort |
Matt Kaufmann |
title |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
title_short |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
title_full |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
title_fullStr |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
title_full_unstemmed |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
title_sort |
how can i do that with acl2? recent enhancements to acl2 |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2011-10-01 |
description |
The last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-event', 'mbe', and trust tags. In this paper we provide user-level summaries of some ACL2 enhancements introduced after the release of Version 3.5 (in May, 2009, at about the time of the 2009 ACL2 workshop) up through the release of Version 4.3 in July, 2011, roughly a couple of years later. Many of these features are not particularly well known yet, but most ACL2 users could take advantage of at least some of them. Some of the changes could affect existing proof efforts, such as a change that treats pairs of functions such as 'member' and 'member-equal' as the same function. |
url |
http://arxiv.org/pdf/1110.4673v1 |
work_keys_str_mv |
AT mattkaufmann howcanidothatwithacl2recentenhancementstoacl2 AT jstrothermoore howcanidothatwithacl2recentenhancementstoacl2 |
_version_ |
1725560702792368128 |