Advertisement

Hygienic Macros for ACL2

  • Carl Eastlund
  • Matthias Felleisen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6546)

Abstract

ACL2 is a theorem prover for a purely functional subset of Common Lisp. It inherits Common Lisp’s unhygienic macros, which are used pervasively to eliminate repeated syntactic patterns. The lack of hygiene means that macros do not automatically protect their producers or consumers from accidental variable capture. This paper demonstrates how this lack of hygiene interferes with theorem proving. It then explains how to design and implement a hygienic macro system for ACL2. An evaluation of the ACL2 code base shows the potential impact of this hygienic macro system on existing libraries and practices.

Keywords

Free Variable Theorem Prove Source Program Common Lisp Unique Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: an Approach. Kluwer Academic Publishers, Dordrecht (2000)Google Scholar
  2. 2.
    Kaufmann, M., Moore, J.S.: Design goals of ACL2. Technical report, Computational Logic, Inc. (1994)Google Scholar
  3. 3.
    Kohlbecker, E., Friedman, D.P., Felleisen, M., Duba, B.: Hygienic macro expansion. In: Proc. 1986 ACM Conference on LISP and Functional Programming, pp. 151–161. ACM Press, New York (1986)CrossRefGoogle Scholar
  4. 4.
    Clinger, W., Rees, J.: Macros that work. In: Proc. 18th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 155–162. ACM Press, New York (1991)Google Scholar
  5. 5.
    Dybvig, R.K., Hieb, R., Bruggeman, C.: Syntactic abstraction in Scheme. Lisp and Symbolic Computation 5(4), 295–326 (1992)CrossRefGoogle Scholar
  6. 6.
    Herman, D., Wand, M.: A theory of hygienic macros. In: Gairing, M. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 48–62. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Flatt, M.: Composable and compilable macros: you want it when? In: Proc. 7th ACM SIGPLAN International Conference on Functional Programming, pp. 72–83. ACM Press, New York (2002)Google Scholar
  8. 8.
    Kaufmann, M., Moore, J.S.: ACL2 Documentation (2009), http://userweb.cs.utexas.edu/users/moore/acl2/current/acl2-doc.html
  9. 9.
    Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference (2001), http://pvs.csl.sri.com/doc/pvs-language-reference.pdf
  10. 10.
    Danielsson, N.A., Norell, U.: Parsing mixfix operators. In: Proc. 20th International Symposium on the Implementation and Application of Functional Languages, School of Computer Science of the University of Hertfordshire (2008)Google Scholar
  11. 11.
    Wenzel, M.: The Isabelle/Isar Reference Manual (2010), http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf
  12. 12.
    Griffin, T.G.: Notational definition—a formal account. In: Proc. 3rd Annual Symposium on Logic in Computer Science, pp. 372–383. IEEE Press, Los Alamitos (1988)Google Scholar
  13. 13.
    The Coq Development Team: The Coq Proof Assistant Reference Manual (2009), http://coq.inria.fr/coq/distrib/current/refman/
  14. 14.
    Kelsey, R., Clinger, W., Rees, J. (eds.): Revised5 report on the algorithmic language Scheme. ACM SIGPLAN Notices 33(9), 26–76 (1998)CrossRefGoogle Scholar
  15. 15.
    Gray, K., Flatt, M.: Compiling Java to PLT Scheme. In: Proc. 5th Workshop on Scheme and Functional Programming, pp. 53–61 (2004)Google Scholar
  16. 16.
    Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of Typed Scheme. In: Proc. 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 395–406. ACM Press, New York (2008)CrossRefGoogle Scholar
  17. 17.
    Vaillancourt, D., Page, R., Felleisen, M.: ACL2 in DrScheme. In: Proc. 6th International Workshop on the ACL2 Theorem Prover and its Applications, pp. 107–116 (2006)Google Scholar
  18. 18.
    Culpepper, R.: Refining Syntactic Sugar: Tools for Supporting Macro Development. PhD dissertation, Northeastern University (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Carl Eastlund
    • 1
  • Matthias Felleisen
    • 1
  1. 1.Northeastern UniversityBostonUSA

Personalised recommendations