{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:38Z","timestamp":1740123278236,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2017,2,1]],"date-time":"2017-02-01T00:00:00Z","timestamp":1485907200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004836","name":"Det Frie Forskningsr\u00e5d","doi-asserted-by":"publisher","award":["DFF-1323-00247"],"award-info":[{"award-number":["DFF-1323-00247"]}],"id":[{"id":"10.13039\/501100004836","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10817-017-9405-9","type":"journal-article","created":{"date-parts":[[2017,2,1]],"date-time":"2017-02-01T08:16:27Z","timestamp":1485936987000},"page":"425-454","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formally Proving Size Optimality of Sorting Networks"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7866-7484","authenticated-orcid":false,"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim S.","family":"Larsen","sequence":"additional","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":[[2017,2,1]]},"reference":[{"key":"9405_CR1","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1215\/ijm\/1256049011","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."},{"issue":"1","key":"9405_CR2","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1007\/BF03023914","volume":"8","author":"K Appel","year":"1986","unstructured":"Appel, K., Haken, W.: The four color proof suffices. Math. Intell. 8(1), 10\u201320 (1986)","journal-title":"Math. Intell."},{"key":"9405_CR3","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1215\/ijm\/1256049012","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."},{"key":"9405_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science. Springer, Berlin (2004)"},{"key":"9405_CR5","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21, 827\u2013859 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9405_CR6","doi-asserted-by":"crossref","unstructured":"Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): Interactive Theorem Proving, ITP 2013, Proceedings, LNCS, vol. 7998. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39634-2"},{"key":"9405_CR7","doi-asserted-by":"crossref","unstructured":"Bundala, D., Z\u00e1vodn\u00fd, J.: Optimal sorting networks. In: A.H. Dediu, C.\u00a0Mart\u00edn-Vide, J.L. Sierra-Rodr\u00edguez, B.\u00a0Truthe (eds.) LATA, LNCS, vol. 8370, pp. 236\u2013247. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-04921-2_19"},{"issue":"1","key":"9405_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0012-365X(90)90173-F","volume":"81","author":"MJ Chung","year":"1990","unstructured":"Chung, M.J., Ravikumar, B.: Bounds on the size of test sets for sorting and related networks. Discrete Math. 81(1), 1\u20139 (1990)","journal-title":"Discrete Math."},{"key":"9405_CR9","doi-asserted-by":"crossref","unstructured":"Claret, G., Gonz\u00e1lez-Huesca, L., R\u00e9gis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In: Blazy et\u00a0al. [6], pp. 67\u201383","DOI":"10.1007\/978-3-642-39634-2_8"},{"key":"9405_CR10","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"},{"issue":"3","key":"9405_CR11","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1016\/j.jcss.2015.11.014","volume":"82","author":"M Codish","year":"2016","unstructured":"Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Sorting nine inputs requires twenty-five comparisons. J. Comput. Syst. Sci. 82(3), 551\u2013563 (2016)","journal-title":"J. Comput. Syst. Sci."},{"key":"9405_CR12","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.\u00a010, pp. 21\u201330. Schloss Dagstuhl (2011). http:\/\/www.dagstuhl.de\/dagpub\/978-3-939897-30-9"},{"issue":"1","key":"9405_CR13","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.entcs.2005.11.024","volume":"151","author":"L Cruz-Filipe","year":"2006","unstructured":"Cruz-Filipe, L., Letouzey, P.: A large-scale experiment in executing extracted programs. Electron. Notes Comput. Sci. 151(1), 75\u201391 (2006)","journal-title":"Electron. Notes Comput. Sci."},{"key":"9405_CR14","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Formalizing size-optimal sorting networks: extracting a certified proof checker. In: C.\u00a0Urban, X.\u00a0Zhang (eds.) ITP 2015, LNCS, vol. 9236, pp. 154\u2013169. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-22102-1_10"},{"key":"9405_CR15","doi-asserted-by":"crossref","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, LNAI, vol. 9150, pp. 55\u201370. Springer (2015)","DOI":"10.1007\/978-3-319-20615-8_4"},{"key":"9405_CR16","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Wiedijk, F.: Hierarchical reflection. In: Slind, K., Bunker, A., Gopalakrishnan,G. (eds.) TPHOLs, LNCS, vol. 3223, pp. 66\u201381. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30142-4_5"},{"key":"9405_CR17","doi-asserted-by":"crossref","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: ICTAC, Lecture Notes in Computer Science, vol. 6255, pp. 260\u2013274. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14808-8_18"},{"key":"9405_CR18","unstructured":"Erk\u00f6k, L., Matthews, J.: Using Yices as an automated solver in Isabelle\/HOL. In: Automated Formal Methods\u201908, pp. 3\u201313. ACM Press, Princeton, NJ, USA (2008)"},{"key":"9405_CR19","doi-asserted-by":"crossref","unstructured":"Floyd, R., Knuth, D.: The Bose\u2013Nelson sorting problem. In: Srivastava, J. N. (ed.) A Survey of Combinatorial Theory, pp. 163\u2013172. North-Holland, Amsterdam (1973)","DOI":"10.1016\/B978-0-7204-2262-7.50020-X"},{"key":"9405_CR20","doi-asserted-by":"crossref","unstructured":"Fouilh\u00e9, A., Monniaux, D., P\u00e9rin, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., \u00e4hndrich, M.F (eds.) SAS 2013, LNCS, vol. 7935, pp. 345\u2013365. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38856-9_19"},{"issue":"11","key":"9405_CR21","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. Not. AMS 55(11), 1382\u20131393 (2008)","journal-title":"Not. AMS"},{"key":"9405_CR22","doi-asserted-by":"crossref","unstructured":"Harrison, J.: HOL Light: a tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) FMCAD, Lecture Notes in Computer Science, vol. 1166, pp. 265\u2013269. Springer, Berlin (1996)","DOI":"10.1007\/BFb0031814"},{"issue":"3","key":"9405_CR23","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A skeptic\u2019s approach to combining HOL and maple. J. Autom. Reason. 21(3), 279\u2013294 (1998)","journal-title":"J. Autom. Reason."},{"key":"9405_CR24","doi-asserted-by":"crossref","unstructured":"Heule, M., Kullmann, O., Marek, V.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le\u00a0Berre, D. (eds.) SAT 2016, Lecture Notes in Computer Science, vol. 9710, pp. 228\u2013245. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"9405_CR25","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1016\/0196-6774(82)90026-8","volume":"3","author":"DS Johnson","year":"1982","unstructured":"Johnson, D.S.: The np-completeness column: an ongoing guide. J. Algorithms 3, 288\u2013300 (1982)","journal-title":"J. Algorithms"},{"key":"9405_CR26","volume-title":"The Art of Computer Programming, Volume III: Sorting and Searching","author":"D Knuth","year":"1973","unstructured":"Knuth, D.: The Art of Computer Programming, Volume III: Sorting and Searching. Springer, Reading (1973)"},{"key":"9405_CR27","doi-asserted-by":"crossref","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: C.\u00a0Sinz, U.\u00a0Egly (eds.) SAT 2014, LNCS, vol. 8561, pp. 219\u2013226. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-09284-3_17"},{"key":"9405_CR28","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Spitters, B.: Computer certified efficient exact reals in Coq. In: Davenport, J., Farmer, W., Urban, J., Rabe, F. (eds.) Calculemus 2011, LNCS, vol. 6824, pp. 90\u2013106. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22673-1_7"},{"issue":"7","key":"9405_CR29","doi-asserted-by":"crossref","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":"9405_CR30","doi-asserted-by":"crossref","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, Berlin (2008)","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"9405_CR31","doi-asserted-by":"crossref","unstructured":"McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES, LNCS, vol. 2277, pp. 197\u2013216. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45842-5_13"},{"key":"9405_CR32","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)"},{"key":"9405_CR33","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology (2007)"},{"key":"9405_CR34","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, R.: Certified exact transcendental real number computation in Coq. In: Mohamed, O., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008, LNCS, vol. 5170, pp. 246\u2013261. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71067-7_21"},{"key":"9405_CR35","doi-asserted-by":"crossref","unstructured":"Oury, N.: Observational equivalence and program extraction in the Coq proof assistant. In: Hofmann, M. (ed.) TLCA 2003, LNCS, vol. 2701, pp. 271\u2013285. Springer, Berlin (2003)","DOI":"10.1007\/3-540-44904-3_19"},{"issue":"2","key":"9405_CR36","doi-asserted-by":"crossref","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. Theory 24(2), 101\u2013116 (1991)","journal-title":"Math. Syst. Theory"},{"key":"9405_CR37","doi-asserted-by":"crossref","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Benzm\u00fcller, C., Paleo, B. (eds.) UITP 2014, EPTCS, vol. 167, pp. 61\u201372 (2014)","DOI":"10.4204\/EPTCS.167.8"},{"key":"9405_CR38","doi-asserted-by":"crossref","unstructured":"Thiemann, R.: Formalizing bounded increase. In: Blazy et\u00a0al. [6], pp. 245\u2013260","DOI":"10.1007\/978-3-642-39634-2_19"},{"issue":"3","key":"9405_CR39","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1016\/0020-0190(77)90031-X","volume":"6","author":"P Emde Boas van","year":"1977","unstructured":"van Emde Boas, P.: Preserving order in a forest in less than logarithmic time and linear space. Inf. Process. Lett. 6(3), 80\u201382 (1977)","journal-title":"Inf. Process. Lett."},{"key":"9405_CR40","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/978-1-4684-2001-2_12","volume-title":"Complexity of Computer Computations, The IBM Research Symposia Series","author":"D Voorhis Van","year":"1972","unstructured":"Van Voorhis, D.: Toward a lower bound for sorting networks. In: Miller, R., Thatcher, J. (eds.) Complexity of Computer Computations, The IBM Research Symposia Series, pp. 119\u2013129. Plenum Press, New York (1972)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9405-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9405-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9405-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T00:56:40Z","timestamp":1568768200000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9405-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,1]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["9405"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9405-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,2,1]]}}}