{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:05:24Z","timestamp":1770285924031,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_8","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T10:23:14Z","timestamp":1278930194000},"page":"83-98","source":"Crossref","is-referenced-by-count":34,"title":["Extending Coq with Imperative Features and Its Application to SAT Verification"],"prefix":"10.1007","author":[{"given":"Micha\u00ebl","family":"Armand","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Arnaud","family":"Spiwack","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Baker, H.G.: Shallow Binding Makes Functional Arrays Fast. ACM SIGPLAN notices\u00a026, 145\u2013147 (1991)","DOI":"10.1145\/122598.122614"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11538363_12","volume-title":"Computer Science Logic","author":"B. Barras","year":"2005","unstructured":"Barras, B., Gr\u00e9goire, B.: On the Role of Type Decorations in the Calculus of Inductive Constructions. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 151\u2013166. Springer, Heidelberg (2005)"},{"key":"8_CR3","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","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, Heidelberg (2004)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/3-540-45587-6_3","volume-title":"Practical Aspects of Declarative Languages","author":"R.S. Boyer","year":"2002","unstructured":"Boyer, R.S., Moore, J.S.: Single-Threaded Objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol.\u00a02257, pp. 9\u201327. Springer, Heidelberg (2002)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative Functional Programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 134\u2013149. Springer, Heidelberg (2008)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Conchon, S., Filli\u00e2tre, J.-C.: A persistent union-find data structure. In: ACM Workshop on ML, pp. 37\u201346 (2007)","DOI":"10.1145\/1292535.1292541"},{"key":"8_CR7","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Formalizing a SAT Proof Checker in Coq. First Coq Workshop, published as technical report tum-i0919 of the Technical University of Munich (2009)"},{"key":"8_CR8","unstructured":"Gonthier, G.: Formal Proof \u2013 The Four-Color Theorem. Notices of the AMS\u00a055(11) (2008)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP, pp. 235\u2013246 (2002)","DOI":"10.1145\/581478.581501"},{"key":"8_CR10","series-title":"Texts in Theoretical Computer Science","volume-title":"Decision Procedures, An Algorithmic Point of View","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures, An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer, Heidelberg (2008)"},{"key":"8_CR11","unstructured":"Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA (1990)"},{"key":"8_CR12","unstructured":"Leroy, X.: Objective Caml (1997), \n                    \n                      http:\/\/ocaml.inria.fr\/"},{"key":"8_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104","volume-title":"Purely Functional Data Structures","author":"C. Okasaki","year":"1998","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45607-4_1","volume-title":"Logic Based Program Synthesis and Transformation","author":"N. Shankar","year":"2002","unstructured":"Shankar, N.: Static Analysis for Safe Destructive Updates in a Functional Language. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol.\u00a02372, pp. 1\u201324. Springer, Heidelberg (2002)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/978-3-642-03359-9_30","volume-title":"TPHOLs\u201909","author":"W. Swierstra","year":"2009","unstructured":"Swierstra, W.: A Hoare Logic for the State Monad. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 440\u2013451. Springer, Heidelberg (2009)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-540-71067-7_25","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Th\u00e9ry","year":"2008","unstructured":"Th\u00e9ry, L.: Proof Pearl: Revisiting the Mini-Rubik in Coq. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 310\u2013319. Springer, Heidelberg (2008)"},{"key":"8_CR17","unstructured":"Princeton University. zChaff, \n                    \n                      http:\/\/www.princeton.edu\/~chaff\/zchaff.html"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P. Wadler","year":"1995","unstructured":"Wadler, P.: Monads for Functional Programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol.\u00a0925, pp. 24\u201352. Springer, Heidelberg (1995)"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T. Weber","year":"2009","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. Applied Logic\u00a07(1), 26\u201340 (2009)","journal-title":"J. Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T08:17:25Z","timestamp":1619770645000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}