{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:52:30Z","timestamp":1742957550671,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319221014"},{"type":"electronic","value":"9783319221021"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_10","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"154-169","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"10_CR1","first-page":"429","volume":"21","author":"K Appel","year":"1977","unstructured":"Appel, K., Haken, W.: Every planar map is four colorable. Part I: discharging. Ill. J. Math. 21, 429\u2013490 (1977)","journal-title":"Ill. J. Math."},{"key":"10_CR2","first-page":"491","volume":"21","author":"K Appel","year":"1977","unstructured":"Appel, K., Haken, W., Koch, J.: Every planar map is four colorable. Part II: reducibility. Ill. J. Math. 21, 491\u2013567 (1977)","journal-title":"Ill. J. Math."},{"issue":"1835","key":"10_CR3","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Trans. A Roy. Soc. 363(1835), 2351\u20132375 (2005)","journal-title":"Trans. A Roy. Soc."},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Theorem Proving","year":"2013","unstructured":"Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): ITP 2013. LNCS, vol. 7998. Springer, Heidelberg (2013)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Claret, G., Gonz\u00e1lez-Huesca, L.C., R\u00e9gis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In Blazy et al. [4], pp. 67\u201383","DOI":"10.1007\/978-3-642-39634-2_8"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Twenty-five comparators is optimal when sorting nine inputs (and twenty-nine for ten). In: ICTAI 2014, pp. 186\u2013193. IEEE (2014)","DOI":"10.1109\/ICTAI.2014.36"},{"key":"10_CR7","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schau\u00df, M., (ed.) RTA 2011. LIPIcs, vol. 10, pp. 21\u201330. Schloss Dagstuhl (2011)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-20615-8_4","volume-title":"Intelligent Computer Mathematics","author":"L Cruz-Filipe","year":"2015","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Optimizing a certified proof checker for a large-scale computer-generated proof. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 55\u201370. Springer, Heidelberg (2015)"},{"key":"10_CR9","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/B978-0-7204-2262-7.50020-X","volume-title":"A Survey of Combinatorial Theory","author":"RW Floyd","year":"1973","unstructured":"Floyd, R.W., Knuth, D.E.: The Bose-Nelson sorting problem. In: Srivastava, J.N. (ed.) A Survey of Combinatorial Theory, pp. 163\u2013172. North-Holland, Amsterdam (1973)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38856-9_19","volume-title":"Static Analysis","author":"A Fouilhe","year":"2013","unstructured":"Fouilhe, A., Monniaux, D., P\u00e9rin, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 345\u2013365. Springer, Heidelberg (2013)"},{"issue":"11","key":"10_CR11","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof - the four-color theorem. Not. AMS 55(11), 1382\u20131393 (2008)","journal-title":"Not. AMS"},{"key":"10_CR12","series-title":"Sorting and Searching","volume-title":"The Art of Computer Programming","author":"DE Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming. Sorting and Searching, vol. 3. Addison-Wesley, Reading (1973)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-319-09284-3_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Konev","year":"2014","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219\u2013226. Springer, Heidelberg (2014)"},{"issue":"7","key":"10_CR14","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"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/BF02090393","volume":"24","author":"I Parberry","year":"1991","unstructured":"Parberry, I.: A computer-assisted optimal depth lower bound for nine-input sorting networks. Math. Syst. Theor. 24(2), 101\u2013116 (1991)","journal-title":"Math. Syst. Theor."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Benzm\u00fcller, C., Paleo, B.W. (eds.) UITP 2014. EPTCS, vol. 167, pp. 61\u201372 (2014)","DOI":"10.4204\/EPTCS.167.8"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Thiemann, R.: Formalizing bounded increase. In: Blazy et al. [4], pp. 245\u2013260","DOI":"10.1007\/978-3-642-39634-2_19"},{"key":"10_CR18","series-title":"The IBM Research Symposia Series","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-1-4684-2001-2_12","volume-title":"Complexity of Computer Computations","author":"DC van Voorhis","year":"1972","unstructured":"van Voorhis, D.C.: Toward a lower bound for sorting networks. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations. The IBM Research Symposia Series, pp. 119\u2013129. Plenum Press, New York (1972)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T06:02:19Z","timestamp":1676959339000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}