{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T04:04:42Z","timestamp":1750478682519,"version":"3.41.0"},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.<\/jats:p>","DOI":"10.1017\/s0956796807006338","type":"journal-article","created":{"date-parts":[[2007,4,23]],"date-time":"2007-04-23T14:33:49Z","timestamp":1177338829000},"page":"15-46","source":"Crossref","is-referenced-by-count":26,"title":["Efficient execution in an automated reasoning environment"],"prefix":"10.1017","volume":"18","author":[{"given":"DAVID A.","family":"GREVE","sequence":"first","affiliation":[]},{"given":"MATT","family":"KAUFMANN","sequence":"additional","affiliation":[]},{"given":"PANAGIOTIS","family":"MANOLIOS","sequence":"additional","affiliation":[]},{"given":"J STROTHER","family":"MOORE","sequence":"additional","affiliation":[]},{"given":"SANDIP","family":"RAY","sequence":"additional","affiliation":[]},{"given":"JOS\u00c9 LUIS","family":"RUIZ-REINA","sequence":"additional","affiliation":[]},{"given":"ROB","family":"SUMNERS","sequence":"additional","affiliation":[]},{"given":"DARON","family":"VROON","sequence":"additional","affiliation":[]},{"given":"MATTHEW","family":"WILDING","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,1,1]]},"reference":[{"key":"S0956796807006338_manual_ref-27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_19"},{"key":"S0956796807006338_manual_ref-1","first-page":"95","volume-title":"Fifth Annual IEEE Symposium on Logic in Computer Science","author":"Allen","year":"1990"},{"key":"S0956796807006338_manual_ref-25","unstructured":"Manolios, P. & Kaufmann, M. (2002) Adding a total order to ACL2. In: Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications, Borrione, D. , Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2002\/"},{"key":"S0956796807006338_manual_ref-33","unstructured":"Ray, S. (2004) Attaching efficient executability to partial functions in ACL2. In: Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2004\/"},{"key":"S0956796807006338_manual_ref-15","unstructured":"Greve, D. & Wilding, M. (2003) Using MBE to speed a verified graph pathfinder. In: Proceedings of the 4th International Workshop on the ACL2 Theorem Prover and Its Applications, Hunt, W. A. Jr. , Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/"},{"key":"S0956796807006338_manual_ref-37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0_13"},{"key":"S0956796807006338_manual_ref-17","unstructured":"Greve, D. A. , Kaufmann, M. , Manolios, P. , Moore, J S. , Ray, S. , Ruiz-Reina, J. L. , Sumners, R. , Vroon, D. & Wilding, M. (2006) Efficient Execution in an Automated Reasoning Environment. Tech. rept. TR-06-59. Department of Computer Sciences, University of Texas at Austin. Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/acl2-papers.-html#Utilities"},{"volume-title":"Common Lisp the Language.","year":"1990","author":"Steele","key":"S0956796807006338_manual_ref-40"},{"key":"S0956796807006338_manual_ref-41","unstructured":"Sumners, R. (2000) Correctness proof of a BDD manager in the context of satisfiability checking. In: Proceedings of the 2nd International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2000\/"},{"key":"S0956796807006338_manual_ref-14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_19"},{"key":"S0956796807006338_manual_ref-29","first-page":"1","article-title":"Ordinal arithmetic: Algorithms and mechanization","volume":"34","author":"Manolios","year":"2006","journal-title":"J. Automated Reasoning"},{"volume-title":"The Correctness Problem in Computer Science.","year":"1981","author":"Boyer","key":"S0956796807006338_manual_ref-5"},{"key":"S0956796807006338_manual_ref-38","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569883"},{"key":"S0956796807006338_manual_ref-31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_27"},{"volume-title":"Efficiently Executing","year":"1999","author":"Shankar","key":"S0956796807006338_manual_ref-39"},{"volume-title":"Development and Analysis of the Software Implemented Fault Tolerance (Sift) Computer.","year":"1984","author":"Goldberg","key":"S0956796807006338_manual_ref-13"},{"key":"S0956796807006338_manual_ref-22","unstructured":"Kaufmann, M & Moore, J S. (2006) ACL2 Home Page. Available at: !http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"S0956796807006338_manual_ref-7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45587-6_3"},{"key":"S0956796807006338_manual_ref-20","unstructured":"Kaufmann, M. & Moore, J S. (1997) A precise description of the ACL2 logic. Tech. rept. Department of Computer Sciences, University of Texas at Austin. See URL: http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/acl2-papers.-html#Foundations."},{"volume-title":"A Computational Logic.","year":"1979","author":"Boyer","key":"S0956796807006338_manual_ref-4"},{"key":"S0956796807006338_manual_ref-18","unstructured":"Harrison, J. (1995) Metatheory and Reflection in Theorem Proving: A Survey and Critique. Tech. rept. CRC-053. SRI International Cambridge Computer Science Research Centre. Available at: http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/reflect.html"},{"key":"S0956796807006338_manual_ref-16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0_8"},{"key":"S0956796807006338_manual_ref-8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0523-7_5"},{"key":"S0956796807006338_manual_ref-26","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000009505.07087.34"},{"key":"S0956796807006338_manual_ref-32","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(06)80007-6"},{"key":"S0956796807006338_manual_ref-19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57960-5"},{"key":"S0956796807006338_manual_ref-35","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9030-5"},{"key":"S0956796807006338_manual_ref-24","doi-asserted-by":"publisher","DOI":"10.1145\/858570.858572"},{"key":"S0956796807006338_manual_ref-42","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(80)90015-6"},{"key":"S0956796807006338_manual_ref-12","unstructured":"Davis, J. (2004) Finite set theory based on fully ordered lists. In: Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2004\/"},{"key":"S0956796807006338_manual_ref-34","unstructured":"Ray, S. & Sumners, R. (2002) Verification of an in-place quicksort in ACL2. In: Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications, Borrione, D. , Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2002\/"},{"key":"S0956796807006338_manual_ref-9","first-page":"275","volume-title":"Proceedings of the 1st International Conference on Formal Methods in Computer-Aided Design (FMCAD 1996).","author":"Brock","year":"1996"},{"key":"S0956796807006338_manual_ref-23","unstructured":"Kaufmann, M. & Sumners, R. (2002) Efficient rewriting of data structures in ACL2. In: Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications, Borrione, D. , Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2002\/"},{"volume-title":"Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2004","year":"2004","author":"Manolios","key":"S0956796807006338_manual_ref-28"},{"key":"S0956796807006338_manual_ref-11","unstructured":"Crow, J. , Owre, S. , Rushby, J. , Shankar, N. & Stringer-Calvert, D. (2001) Evaluating, Testing, and Animating PVS Specifications. Tech. rept. Menlo Park, CA: Computer Science Laboratory, SRI International. Available at: http:\/\/www.csl.sri.com\/users\/rushby\/papers\/attach.pdf"},{"volume-title":"A Computational Logic Handbook","year":"1997","author":"Boyer","key":"S0956796807006338_manual_ref-6"},{"key":"S0956796807006338_manual_ref-2","first-page":"409","article-title":"Special issue on system verification","volume":"5","author":"Bevier","year":"1989","journal-title":"J. Automated Reasoning"},{"key":"S0956796807006338_manual_ref-21","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026517200045"},{"key":"S0956796807006338_manual_ref-3","doi-asserted-by":"publisher","DOI":"10.1145\/321864.321875"},{"key":"S0956796807006338_manual_ref-10","unstructured":"Cowles, J. , Gamboa, R. & van Baalen, J. (2003) Using ACL2 arrays to formalize matrix algebra. In: Proceedings of the 4th International Workshop on the ACL2 Theorem Prover and Its Applications, Hunt, W. A. Jr. , Kaufmann, M. & Moore, J S. (eds), Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/"},{"key":"S0956796807006338_manual_ref-30","unstructured":"Matthews, J. & Vroon, D. (2004) Partial clock functions in ACL2. Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2004\/"},{"key":"S0956796807006338_manual_ref-36","unstructured":"Russinoff, D. , Kaufmann, M. , Smith, E. & Sumners, R. (July 2005) Formal verification of floating-point RTL at amd using the ACL2 theorem prover. In: Proceedings of the 17th IMACS World Congress on Scientific Computation, Applied Mathematics and Simulation, Simonov, N. (ed). Available at: http:\/\/sab.sscc.ru\/imacs2005\/papers\/T2-I-94-1021.pdf"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006338","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T16:47:33Z","timestamp":1750438053000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006338\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["S0956796807006338"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006338","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"type":"print","value":"0956-7968"},{"type":"electronic","value":"1469-7653"}],"subject":[],"published":{"date-parts":[[2008,1]]}}}