Abstract
Boyer and Moore’s ACL2 theorem prover combines first-order applicative Common Lisp with a computational, first-order logic. While ACL2 has become popular and is being used for large programs, ACL2 forces programmers to rely on manually maintained protocols for managing modularity. In this paper, we present a prototype of Modular ACL2. The system extends ACL2 with a simple, but pragmatic functional module system. We provide an informal introduction, sketch a formal semantics, and report on our first experiences.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Boyer, R.S., Moore, J.S.: Mechanized reasoning about programs and computing machines. In: Veroff, R. (ed.) Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pp. 146–176. MIT Press, Cambridge (1996)
Steele Jr., G.L.: Common Lisp—The Language. Digital Press (1984)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)
Harper, R., Pierce, B.C.: Design considerations for ML-style module systems. In: Advanced Topics in Types and Prog. Languages, pp. 293–345. MIT Press, Cambridge (2004)
Page, R.: Engineering software correctness. J. of Func. Prog. 17(6), 675–686 (2007)
Vaillancourt, D., Page, R., Felleisen, M.: ACL2 in DrScheme. In: Proc. 6th Intern. Works. ACL2 Theorem Prover and its Applications, pp. 107–116. ACM Press, New York (2006)
Eastlund, C., Vaillancourt, D., Felleisen, M.: ACL2 for freshmen: First experiences. In: Proc. 7th Intern. ACL2 Workshop, pp. 200–211. ACM Press, New York (2007)
Flatt, M., Felleisen, M.: Units: Cool modules for HOT languages. In: ACM SIGPLAN Conference on Prog. Language Design and Implementation, pp. 236–248 (June 1998)
Owens, S., Flatt, M.: From structures and functors to modules and units. In: ACM SIGPLAN Intern. Conference on Func. Prog., pp. 87–98. ACM Press, New York (2006)
Bracha, G., Lindstrom, G.: Modularity meets inheritance. In: Proceedings of the International Conference on Computer Languages, pp. 282–290. IEEE, Los Alamitos (1992)
Dreyer, D., Rossberg, A.: Mixin’ up the ML module system. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 307–320. ACM, New York (2008)
Chrzaszcz, J.: Implementing modules in the Coq system. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 270–286. Springer, Heidelberg (2003)
Courant, J.: \(\mathcal{MC}_2\): A Module Calculus for Pure Type Systems. J. of Func. Prog. 17, 287–352 (2006)
Harper, R., Pfenning, F.: A module system for a programming language based on the LF logical framework. Journal of Logic and Computation 8(1), 5–31 (1998)
Sannella, D.: Formal program development in Extended ML for the working programmer. In: Proc. 3rd BCS/FACS Workshop on Refinement, pp. 99–130 (1991)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (2e). MIT Press, Cambridge (1990)
Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149–166. Springer, Heidelberg (1999)
The Coq Development Team: The Coq Proof Assistant Reference Manual (2006), http://coq.inria.fr/V8.1pl3/refman/index.html
Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: An interactive mathematical proof system. Journal of Automated Reasoning 11, 213–248 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eastlund, C., Felleisen, M. (2008). Toward a Practical Module System for ACL2. In: Gill, A., Swift, T. (eds) Practical Aspects of Declarative Languages. PADL 2009. Lecture Notes in Computer Science, vol 5418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92995-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-92995-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-92994-9
Online ISBN: 978-3-540-92995-6
eBook Packages: Computer ScienceComputer Science (R0)