Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Practical Aspects of Declarative Languages

PADL 2002: Practical Aspects of Declarative Languages pp 9–27Cite as

Single-Threaded Objects in ACL2

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2257))

Abstract

ACL2 is a first-order applicative programming language based on Common Lisp. It is also a mathematical logic for which a mechanical theorem-prover has been implemented in the style of the Boyer-Moore theorem prover. The ACL2 system is used primarily in the modeling and verification of computer hardware and software, where the executability of the language allows models to be used as prototype designs or “simulators.” To support efficient execution of certain kinds of models, especially models of microprocessors, ACL2 provides “singlethreaded objects,” structures with the usual “copy on write” applicative semantics but for which writes are implemented destructively. Syntactic restrictions insure consistency between the formal semantics and the implementation. The design of single-threaded objects has been influenced both by the need to make execution efficient and the need to make proofs about them simple. We discuss the issues.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. In Mathematical Structures in Computer Science 6, pages 579–612. 1996.

    MATH  MathSciNet  Google Scholar 

  2. R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, 1979.

    MATH  Google Scholar 

  3. R. S. Boyer and J S. Moore. A Computational Logic Handbook, Second Edition. Academic Press, New York, 1997.

    Google Scholar 

  4. J.-Y. Girard. Linear logic. In Theoretical Computer Science, volume 50, pages 1–102. 1987.

    Article  MATH  MathSciNet  Google Scholar 

  5. D. Greve, M. Wilding, and D. Hardin. High-speed, analyzable simulators. In Kaufmann et al. [9], pages 113–136.

    Google Scholar 

  6. David A. Greve. Symbolic simulation of the JEM1 microprocessor. In G. Gopalakrishnan and P. Windley, editors, Formal Methods in Computer-Aided Design-FMCAD, LNCS 1522. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  7. David Hardin, Matthew Wilding, and David Greve. Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle. In Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided Verification-CAV’ 98, volume 1427 of Lecture Notes in Computer Science. Springer-Verlag, 1998. See URL http://pobox.com/users/hokie/docs/concept.ps.

    Chapter  Google Scholar 

  8. P. Hudak. Continuation-based mutable abstract data types, or how to have your state and munge it too. Technical Report YaleU/DCS/RR-914, Department of Computer Science, Yale University, July 1992.

    Google Scholar 

  9. M. Kaufmann, P. Manolios, and J S. Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, 2000.

    Google Scholar 

  10. M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Press, 2000.

    Google Scholar 

  11. Matt Kaufmann and J. Moore. A precise description of the acl2 logic. In http://www.cs.utexas.edu/users/moore/publications/km97a.ps.Z. Department of Computer Sciences, University of Texas at Austin, 1997.

  12. J. S. Moore. Rewriting for symbolic execution of state machine models. In Computer-Aided Verification-CAV’01, volume 2102 of Lecture Notes in Computer Science. Springer-Verlag, 2001. See URL http://www.cs.utexas.edu/users/moore/publications/nu-rewriter.

    Google Scholar 

  13. G. Plotkin. Call-by-name, call-by-value, and the λ-calculus. In Theoretical Computer Science, volume 1, pages 125–159. 1975.

    Article  MATH  MathSciNet  Google Scholar 

  14. D. Schmidt. Detecting global variables in denotational specifications. ACM Trans. Prog. Lang, 7:299–310, 1985.

    Article  MATH  Google Scholar 

  15. G. L. Steele, Jr. Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803, 1990.

    Google Scholar 

  16. W. Stoye. Message-based functional operating systems. 6(3):291–311, 1986.

    MATH  Google Scholar 

  17. P. Wadler. Monads for functional programming. In Advanced Functional Programming. Springer Verlag, LNCS 925, 1995.

    Google Scholar 

  18. P. Wadler. How to declare an imperative. ACM Computing Surveys, 29(3):240–263, September 1997.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Sciences, University of Texas at Austin, Taylor Hall 2.124, 78712, Austin, Texas, USA

    Robert S. Boyer & J. Strother Moore

Authors
  1. Robert S. Boyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. Strother Moore
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, Brown University, Box 1910, 02912, Providence, RI, USA

    Shriram Krishnamurthi

  2. Department of Computer Science, SUNY at Stony Brook, 11794-4400, Stony Brook, NY, USA

    C. R. Ramakrishnan

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boyer, R.S., Strother Moore, J. (2002). Single-Threaded Objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds) Practical Aspects of Declarative Languages. PADL 2002. Lecture Notes in Computer Science, vol 2257. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45587-6_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-45587-6_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43092-6

  • Online ISBN: 978-3-540-45587-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation