{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T13:40:09Z","timestamp":1748785209742,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296036"},{"type":"electronic","value":"9783319296043"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29604-3_2","type":"book-chapter","created":{"date-parts":[[2016,2,20]],"date-time":"2016-02-20T12:53:12Z","timestamp":1455972792000},"page":"12-28","source":"Crossref","is-referenced-by-count":3,"title":["From Sets to Bits in Coq"],"prefix":"10.1007","author":[{"given":"Arthur","family":"Blot","sequence":"first","affiliation":[]},{"given":"Pierre-\u00c9variste","family":"Dagand","sequence":"additional","affiliation":[]},{"given":"Julia","family":"Lawall","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,21]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Symposium on Logic in Computer Science (LICS 1990), pp. 95\u2013105 (1990)","DOI":"10.1109\/LICS.1990.113737"},{"key":"2_CR3","unstructured":"Beeler, M., Gosper, R.W., Schroeppel, R.: Hakmem. Tech. report Massachusetts Institute of Technology (1972). http:\/\/hdl.handle.net\/1721.1\/6086"},{"issue":"7","key":"2_CR4","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"BH Bloom","year":"1970","unstructured":"Bloom, B.H.: Space\/time trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422\u2013426 (1970)","journal-title":"Commun. ACM"},{"key":"2_CR5","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Melquiond, G., Paskevich, A.: The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay (2015)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: International Conference on Functional programming (ICFP 2011), pp. 418\u2013430 (2011)","DOI":"10.1145\/2034574.2034828"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"G Klein","year":"2008","unstructured":"Klein, G., Cock, D., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-03545-1_10","volume-title":"Certified Programs and Proofs","author":"C Cohen","year":"2013","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 147\u2013162. Springer, Heidelberg (2013)"},{"key":"2_CR9","unstructured":"Coq Standard Library: Finite sets. https:\/\/coq.inria.fr\/library\/Coq.Sets.Finite_sets.html"},{"key":"2_CR10","unstructured":"Coq Standard Library: Modular implementation of finite sets. https:\/\/coq.inria.fr\/library\/Coq.MSets.MSets.html"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: deductive synthesis of abstract data types in a proof assistant. In: Principles of Programming Languages (POPL 2015), pp. 689\u2013700 (2015)","DOI":"10.1145\/2775051.2677006"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-32347-8_7","volume-title":"Interactive Theorem Proving","author":"M D\u00e9n\u00e8s","year":"2012","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 83\u201398. Springer, Heidelberg (2012)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-27705-4_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J-C Filli\u00e2tre","year":"2012","unstructured":"Filli\u00e2tre, J.-C.: Verifying two lines of C with Why3: an exercise in program verification. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 83\u201397. Springer, Heidelberg (2012)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243\u2013258. Springer, Heidelberg (2010)"},{"key":"2_CR15","unstructured":"Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. Technical report RR-6455, INRIA (2008)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Interactive Theorem Proving","author":"F Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"issue":"4","key":"2_CR17","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1017\/S0956796898003153","volume":"8","author":"M Hedberg","year":"1998","unstructured":"Hedberg, M.: A coherence theorem for Martin-L\u00f6f\u2019s type theory. J. Funct. Program. 8(4), 413\u2013436 (1998)","journal-title":"J. Funct. Program."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Kennedy, A., Benton, N., Jensen, J.B., Dagand, P.E.: Coq: The world\u2019s best macro assembler? In: Symposium on Principles and Practice of Declarative Programming (PPDP 2013), pp. 13\u201324 (2013)","DOI":"10.1145\/2505879.2505897"},{"issue":"7","key":"2_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"2_CR20","unstructured":"Mathematical Components: Finite sets. http:\/\/ssr2.msr-inria.inria.fr\/doc\/mathcomp-1.5\/MathComp.finset.html"},{"key":"2_CR21","unstructured":"M\u00e9rillon, F., R\u00e9veill\u00e8re, L., Consel, C., Marlet, R., Muller, G.: Devil: an IDL for hardware programming. In: Symposium on Operating Systems Design and Implementation (OSDI 2000) (2000)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Conference on Programming Language Design and Implementation (PLDI 2000), pp. 83\u201394 (2000)","DOI":"10.1145\/349299.349314"},{"key":"2_CR23","unstructured":"OCaml Standard Library: Pervasives. http:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/libref\/Pervasives.html"},{"key":"2_CR24","unstructured":"Richards, M.: Backtracking algorithms in MCPL using bit patterns and recursion (1997)"},{"key":"2_CR25","unstructured":"Ssreflect library: Finite type. http:\/\/ssr.msr-inria.inria.fr\/doc\/ssreflect-1.5\/Ssreflect.fintype.html"},{"key":"2_CR26","unstructured":"Ssreflect library: Tuple. http:\/\/ssr.msr-inria.inria.fr\/doc\/mathcomp-1.5\/MathComp.tuple.html"},{"key":"2_CR27","volume-title":"Hacker\u2019s Delight","author":"HS Warren","year":"2012","unstructured":"Warren, H.S.: Hacker\u2019s Delight. Addison-Wesley Professional, Boston (2012)"}],"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-29604-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T13:06:27Z","timestamp":1748783187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29604-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296036","9783319296043"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29604-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}