{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:39:13Z","timestamp":1725975553378},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319906850"},{"type":"electronic","value":"9783319906867"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-90686-7_4","type":"book-chapter","created":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T17:49:55Z","timestamp":1524505795000},"page":"51-67","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Program Extraction for Mutable Arrays"],"prefix":"10.1007","author":[{"given":"Kazuhiko","family":"Sakaguchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,24]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: ICFP 2013, pp. 133\u2013144. ACM (2013)","DOI":"10.1145\/2500365.2500581"},{"key":"4_CR2","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. 5170, pp. 134\u2013149. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_14"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: ICFP 2009, pp. 79\u201390. ACM (2009)","DOI":"10.1145\/1596550.1596565"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Launchbury, J., Peyton Jones, S.L.: Lazy functional state threads. In: PLDI 1994, pp. 24\u201335. ACM (1994)","DOI":"10.1145\/178243.178246"},{"issue":"4","key":"4_CR6","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_12"},{"key":"4_CR8","unstructured":"Letouzey, P.: Programmation fonctionnelle certifi\u00e9e - L\u2019extraction de programmes dans l\u2019assistant Coq. Ph.D. thesis, Universit\u00e9 Paris-Sud (2004)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69407-6_39"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-39634-2_5","volume-title":"Interactive Theorem Proving","author":"A Mahboubi","year":"2013","unstructured":"Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19\u201334. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_5"},{"key":"4_CR11","unstructured":"Mahboubi, A., Tassi, E.: Mathematical components (2016). https:\/\/math-comp.github.io\/mcb\/book.pdf"},{"issue":"5\u20136","key":"4_CR12","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"18","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Prog 18(5\u20136), 865\u2013911 (2008)","journal-title":"J. Funct. Prog"},{"issue":"9","key":"4_CR13","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/1411203.1411237","volume":"43","author":"Aleksandar Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: ICFP 2008, pp. 229\u2013240. ACM (2008)","journal-title":"ACM SIGPLAN Notices"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C.: Extracting $${F}_{\\omega }$$F\u03c9\u2019s programs from proofs in the Calculus of Constructions. In: POPL 1989, pp. 89\u2013104. ACM (1989)","DOI":"10.1145\/75277.75285"},{"issue":"1","key":"4_CR16","first-page":"14","volume":"10","author":"K Sakaguchi","year":"2017","unstructured":"Sakaguchi, K., Kameyama, Y.: Efficient finite-domain function library for the Coq proof assistant. IPSJ Trans. Prog. 10(1), 14\u201328 (2017)","journal-title":"IPSJ Trans. Prog."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F$$^\\star $$\u22c6. In: POPL 2016, pp. 256\u2013270. ACM (2016)","DOI":"10.1145\/2914770.2837655"},{"issue":"2","key":"4_CR18","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"RE Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215\u2013225 (1975)","journal-title":"J. ACM"},{"issue":"2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/62.2160","volume":"31","author":"RE Tarjan","year":"1984","unstructured":"Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245\u2013281 (1984)","journal-title":"J. ACM"},{"key":"4_CR20","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual (2017). https:\/\/coq.inria.fr\/distrib\/V8.7.0\/refman\/"},{"key":"4_CR21","unstructured":"The Mathematical Components Project: The mathematical components repository. https:\/\/github.com\/math-comp\/math-comp"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 925, pp. 24\u201352. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59451-5_2"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-90686-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,16]],"date-time":"2019-10-16T22:29:59Z","timestamp":1571264999000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90686-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319906850","9783319906867"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90686-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}