{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:43:37Z","timestamp":1743151417823,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_31","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"435-450","source":"Crossref","is-referenced-by-count":4,"title":["A Parallelized Theorem Prover for a Logic with Parallel Execution"],"prefix":"10.1007","author":[{"given":"David L.","family":"Rager","sequence":"first","affiliation":[]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J. S : Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Brock, B., Kaufmann, M., Moore, J. S : ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 275\u2013293. Springer, Heidelberg (1996)","DOI":"10.1007\/BFb0031816"},{"key":"31_CR3","unstructured":"Russinoff, D., Kaufmann, M., Smith, E., Sumners, R.: Formal verification of floating-point RTL at AMD using the ACL2 theorem prover. In: Nikolai, S. (ed.) Proceedings of the 17th IMACS World Congrress on Scientific Computation, Applied Mathematics and Simulation, Paris, France (2005)"},{"key":"31_CR4","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-1-4419-1539-9_3","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"W.A. Hunt Jr.","year":"2010","unstructured":"Hunt Jr., W.A., Swords, S., Davis, J., Slobodova, A.: Use of formal verification at Centaur Technology. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 65\u201388. Springer, US (2010)"},{"key":"31_CR5","unstructured":"ACL2: ACL2 Version 6.0 Documentation (December 2012), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v6-0\/acl2-doc.html#User's-Manual"},{"key":"31_CR6","unstructured":"Rager, D.L.: Implementing a parallelism library for ACL2 in modern day Lisps. Master\u2019s thesis, The University of Texas at Austin (2008)"},{"key":"31_CR7","first-page":"18","volume-title":"Proceedings of the 2009 International Lisp Conference","author":"D.L. Rager","year":"2009","unstructured":"Rager, D.L., Hunt Jr., W.A.: Implementing a parallelism library for a functional subset of Lisp. In: Proceedings of the 2009 International Lisp Conference, pp. 18\u201330. Association of Lisp Users, Sterling (2009)"},{"key":"31_CR8","unstructured":"ACL2 Community Books, \n                    \n                      https:\/\/code.google.com\/p\/acl2-books\/"},{"key":"31_CR9","unstructured":"Rager, D.L.: ACL2 6.0 regression suite test configuration details, \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/ragerdl\/papers\/itp2013\/"},{"key":"31_CR10","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/514188.514189","volume":"24","author":"J. S Moore","year":"2002","unstructured":"Moore, J. S , Porter, G.: The apprentice challenge. ACM Transactions on Programming Languages and Systems\u00a024, 193\u2013216 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Verbeek, F., Schmaltz, J.: Formal verification of a deadlock detection algorithm. In: Hardin, D., Schmaltz, J. (eds.) Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, November 3-4. Electronic Proceedings in Theoretical Computer Science, vol.\u00a070, pp. 103\u2013112. Open Publishing Association (2011)","DOI":"10.4204\/EPTCS.70.0"},{"key":"31_CR12","unstructured":"Rager, D.L.: Parallelizing an Interactive Theorem Prover: Functional Programming and Proofs with ACL2. PhD thesis, The University of Texas at Austin (2012)"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/BFb0055144","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Moten","year":"1998","unstructured":"Moten, R.: Exploiting parallelism in interactive theorem provers. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 315\u2013330. Springer, Heidelberg (1998)"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-55160-3_49","volume-title":"Research Directions in High-Level Parallel Programming Languages","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J., Winkler, T.C.: Parallel programmming in Maude. In: Ban\u00e2tre, J.-P., Le M\u00e9tayer, D. (eds.) Research Directions in High-Level Parallel Programming Languages 1991. LNCS, vol.\u00a0574, pp. 253\u2013293. Springer, Heidelberg (1992)"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"841","DOI":"10.1007\/3-540-58156-1_72","volume-title":"Automated Deduction - CADE-12","author":"M.P. Bonacina","year":"1994","unstructured":"Bonacina, M.P., McCune, W.: Distributed theorem proving by peers. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 841\u2013845. Springer, Heidelberg (1994)"},{"key":"31_CR16","unstructured":"Kapur, D., Vandevoorde, M.T.: DLP: a paradigm for parallel interactive theorem proving (1996)"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-52885-7_78","volume-title":"10th International Conference on Automated Deduction","author":"J. Schumann","year":"1990","unstructured":"Schumann, J., Letz, R.: PARTHEO: A high-performance parallel theorem prover. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 40\u201356. Springer, Heidelberg (1990)"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-61511-3_87","volume-title":"Automated Deduction - Cade-13","author":"J. Schumann","year":"1996","unstructured":"Schumann, J.: SicoTHEO: Simple competitive parallel theorem provers. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 240\u2013244. Springer, Heidelberg (1996)"},{"key":"31_CR19","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/1708046.1708058","volume-title":"DAMP 2010: Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming","author":"D.C.J. Matthews","year":"2010","unstructured":"Matthews, D.C.J., Wenzel, M.: Efficient parallel programming in poly\/ML and isabelle\/ML. In: DAMP 2010: Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, pp. 53\u201362. ACM, New York (2010)"},{"key":"31_CR20","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Reis, G.D., Th\u00e9ry, L. (eds.) ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS). ACM Digital library (August 2009)"},{"key":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/978-3-642-39634-2_30","volume-title":"ITP 2013","author":"M. Wenzel","year":"2013","unstructured":"Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 418\u2013434. Springer, Heidelberg (2013)"},{"key":"31_CR22","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, New York (1988)"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Wilding, M.: A parallel version of the Boyer-Moore prover. Technical Report\u00a039. Computational Logic, Inc. (February 1989)","DOI":"10.21236\/ADA207190"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Halstead Jr., R.H.: Implementation of multilisp: Lisp on a microprocessor. In: Conference on Lisp and Functional Programming, pp. 9\u201317 (1984)","DOI":"10.1145\/800055.802017"},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BFb0024154","volume-title":"Parallel Lisp: Languages and Systems","author":"R. Goldman","year":"1990","unstructured":"Goldman, R., Gabriel, R.P., Sexton, C.: Qlisp: An interim report. In: Ito, T., Halstead Jr., R.H. (eds.) US\/Japan WS 1989. LNCS, vol.\u00a0441, pp. 161\u2013181. Springer, Heidelberg (1990)"},{"issue":"3","key":"31_CR26","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/BF01808954","volume":"2","author":"W.L. Harrison","year":"1989","unstructured":"Harrison, W.L.: The interprocedural analysis and automatic parallelization of scheme programs. Lisp and Symbolic Computation\u00a02(3), 179\u2013396 (1989)","journal-title":"Lisp and Symbolic Computation"},{"key":"31_CR27","first-page":"307","volume-title":"Selected Papers of the Second Workshop on Languages and Compilers for Parallel Computing","author":"W.L. Harrison","year":"1990","unstructured":"Harrison, W.L., Ammarguellat, Z.: A comparison of automatic versus manual parallelization of the Boyer-Moore theorem prover. In: Selected Papers of the Second Workshop on Languages and Compilers for Parallel Computing, pp. 307\u2013330. Pitman Publishing, London (1990)"},{"key":"31_CR28","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"31_CR29","unstructured":"University of Cambridge: HOL4 Kananaskis 5 (March 2010), \n                    \n                      http:\/\/hol.sourceforge.net\/"},{"key":"31_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"31_CR31","unstructured":"SRI International: PVS Specification and Verification System (July 2012), \n                    \n                      http:\/\/pvs.csl.sri.com\/"},{"key":"31_CR32","unstructured":"Rager, D.L., Hunt Jr., W.A., Kaufmann, M.: A futures library and parallelism abstractions for a functional subset of Lisp. In: Proceedings of the 4th European Lisp Symposium (March 2011)"},{"key":"31_CR33","doi-asserted-by":"crossref","unstructured":"Schumann, J.: Automated theorem proving in software engineering. Springer (2001)","DOI":"10.1007\/978-3-662-22646-9"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T21:40:56Z","timestamp":1580334056000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}