Making induction manifest in modular ACL2

ABSTRACT

ACL2, a Common Lisp-based language for programming and theorem proving, has enjoyed industrial success despite lacking modern language features such as a module system. In previous work, we equipped ACL2 with modules, interfaces, and explicit linking and measured our system with a series of experiments. One experiment revealed a serious lack of expressivity; the interfaces cannot describe the induction schemes necessary to reason about exported functions with nontrivial patterns of recursion.

In this paper we revise our language, Modular ACL2, to overcome this weakness. The first novelty is the inclusion of manifest function definitions in interfaces from which ACL2 can infer induction schemes. The second novelty consists of the first proofs of soundness and expressivity for Modular ACL2; we also reaffirm the usefulness of our system with updated benchmarks.

REFERENCES

• 1: Chrzaszcz, J. Implementing modules in the Coq system. In Proc. 16th International Conference on Theorem Proving in Higher Order Logics, p. 270--286. Springer, 2003.
• 2: Courant, J. MC2: a module calculus for pure type systems. J. Functional Programming, 17(3):287--352, 2007.
• 3: Culpepper, R., S. Tobin-Hochstadt and M. Flatt. Advanced macrology and the implementation of Typed Scheme. In Proc. 8th Workshop on Scheme and Functional Programming, p. 1--14. ACM Press, 2007.
• 4: Dreyer, D. and A. Rossberg. Mixin' up the ML module system. In Proc. 13th ACM SIGPLAN International Conference on Functional Programming, p. 307--320. ACM Press, 2008.
• 5: Eastlund, C. and M. Felleisen. Toward a practical module system for ACL2. In Proc. 11th International Symposium on Practical Aspects of Declarative Languages, p. 46--60. Springer, 2009.
• 6: Farmer, W.M., J.D. Guttman and F.J. Thayer. IMPS: An interactive mathematical proof system. J. Automated Reasoning, 11(2):213--248, 1993.
• 7: Findler, R.B., J. Clements, C. Flanagan, M. Flatt, S. Krishnamurthi, P. Steckler and M. Felleisen. DrScheme: A programming environment for Scheme. J. Functional Programming, 12(2):159--182, 2002.
• 8: Flatt, M. Composable and compilable macros: You want it when? In Proc. 7th ACM SIGPLAN International Conference on Functional Programming, p. 72--83. ACM Press, 2002.
• 9: Flatt, M. and M. Felleisen. Units: cool modules for HOT languages. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 236--248. ACM Press, 1998.
• 10: Harper, R. and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proc. 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 123--137. ACM Press, 1994.
• 11: Kammüller, F., M. Wenzel and L.C. Paulson. Locales: a sectioning concept for Isabelle. In Proc. 12th International Conference on Theorem Proving in Higher Order Logics, p. 149--166. Springer, 1999.
• 12: Kaufmann, M., P. Manolios and J.S. Moore. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, 2000.
• 13: Kaufmann, M., P. Manolios and J.S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.
• 14: Kaufmann, M. and J.S. Moore. A precise description of the ACL2 logic. Technical report, University of Texas at Austin, 1998.
• 15: Kaufmann, M. and J.S. Moore. Structured theory development for a mechanized logic. J. Automated Reasoning, 26(2):161--203, 2001.
• 16: Leroy, X. Manifest types, modules, and separate compilation. In Proc. 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 109--122. ACM Press, 1994.
• 17: Martín-Mateos, F.J., J.A. Alonso, M.J. Hidalgo and J.L. Ruiz-Reina. A generic instantiation tool and a case study: a generic multiset theory. In Proc. 3rd International Workshop on the ACL2 Theorem Prover and its Applications, p. 188--201. ACM Press, 2002.
• 18: Milner, R., M. Tofte and R. Harper. The Definition of Standard ML. MIT Press, 1990.
• 19: Owens, S. and M. Flatt. From structures and functors to modules and units. In Proc. 11th ACM SIGPLAN International Conference on Functional Programming, p. 87--98. ACM Press, 2006.
• 20: Padget, J. et. al. Desiderata for the standardisation of LISP. In Proc. 1986 ACM Conference on LISP and Functional Programming, p. 54--66. ACM Press, 1986.
• 21: Page, R. Engineering software correctness. J. Functional Programming, 17(6):675--686, 2007.
• 22: Page, R., C. Eastlund and M. Felleisen. Functional programming and theorem proving for undergraduates: a progress report. In Proc. 2008 Workshop on Functional and Declarative Programming in Education, p. 21--30. ACM Press, 2008.
• 23: Sannella, D. Formal program development in Extended ML for the working programmer. In Proc. 3rd BCS/FACS Workshop on Refinement, p. 99--130. Springer, 1991.
• 24: Steele Jr., G.L. Common Lisp--The Language. Digital Press, 1984.
• 25: The Coq Development Team. The Coq Proof Assistant Reference Manual, 2009. http://coq.inria.fr/coq/distrib/current/refman/.
• 26: Vaillancourt, D., R. Page and M. Felleisen. ACL2 in DrScheme. In Proc. 6th International Workshop on the ACL2 Theorem Prover and its Applications, p. 107--116. ACM Press, 2006.
• 27: Wirth, N. Programming in Modula-2. Springer, 1983.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Verification

Keywords:
acl2, module systems, theorem provers