{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:05Z","timestamp":1750221305469,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Austrian Science Fund (FWF)","award":["Y 757"],"award-info":[{"award-number":["Y 757"]}]},{"DOI":"10.13039\/501100009024","name":"Exploratory Research for Advanced Technology","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100009024","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Ministerio de Econom\u00eda y Competitividad","award":["MTM2014-54151-P"],"award-info":[{"award-number":["MTM2014-54151-P"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167103","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"2-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Efficient certification of complexity proofs: formalizing the Perron\u2013Frobenius theorem (invited talk paper)"],"prefix":"10.1145","author":[{"given":"Jose","family":"Divas\u00f3n","sequence":"first","affiliation":[{"name":"University of La Rioja, Spain"}]},{"given":"Sebastiaan","family":"Joosten","sequence":"additional","affiliation":[{"name":"University of Twente, Netherlands"}]},{"given":"Ond\u0159ej","family":"Kun\u010dar","sequence":"additional","affiliation":[{"name":"TU Munich, Germany"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[{"name":"University of Innsbruck, Austria"}]},{"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_24"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693166"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"e_1_3_2_1_4_1","unstructured":"Ferdinand Georg Frobenius. 1912. \u00dcber Matrizen aus nicht negativen Elementen. In Sitzungsberichte Preu\u00df. Akad. Wiss. 456\u2013477.  Ferdinand Georg Frobenius. 1912. \u00dcber Matrizen aus nicht negativen Elementen. In Sitzungsberichte Preu\u00df. Akad. Wiss. 456\u2013477."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"volume-title":"CADE-25 (LNCS)","author":"Giesl J\u00fcrgen","key":"e_1_3_2_1_6_1","unstructured":"J\u00fcrgen Giesl , Fr\u00e9d\u00e9ric Mesnard , Albert Rubio , Ren\u00e9 Thiemann , and Johannes Waldmann . 2015. Termination Competition (termCOMP 2015). In CADE-25 (LNCS) , Vol. 9195 . 105\u2013108. J\u00fcrgen Giesl, Fr\u00e9d\u00e9ric Mesnard, Albert Rubio, Ren\u00e9 Thiemann, and Johannes Waldmann. 2015. Termination Competition (termCOMP 2015). In CADE-25 (LNCS), Vol. 9195. 105\u2013108."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9250-9"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9401-5"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_3_2_1_11_1","volume-title":"ITP 2016 (LNCS)","volume":"9807","author":"Kun\u010dar Ond\u0159ej","year":"2016","unstructured":"Ond\u0159ej Kun\u010dar and Andrei Popescu . 2016 . From Types to Sets by Local Type Definitions in Higher-Order Logic . In ITP 2016 (LNCS) , Vol. 9807 . 200\u2013218. Ond\u0159ej Kun\u010dar and Andrei Popescu. 2016. From Types to Sets by Local Type Definitions in Higher-Order Logic. In ITP 2016 (LNCS), Vol. 9807. 200\u2013218."},{"key":"e_1_3_2_1_12_1","volume-title":"Verified Efficient Implementation of Gabow\u2019s Strongly Connected Components Algorithm. Archive of Formal Proofs (May","author":"Lammich Peter","year":"2014","unstructured":"Peter Lammich . 2014. Verified Efficient Implementation of Gabow\u2019s Strongly Connected Components Algorithm. Archive of Formal Proofs (May 2014 ). http:\/\/isa-afp.org\/entries\/Gabow_SCC.html, Formal proof development. Peter Lammich. 2014. Verified Efficient Implementation of Gabow\u2019s Strongly Connected Components Algorithm. Archive of Formal Proofs (May 2014). http:\/\/isa-afp.org\/entries\/Gabow_SCC.html, Formal proof development."},{"key":"e_1_3_2_1_13_1","volume-title":"LNCS","volume":"2283","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Makarius Wenzel . 2002 . Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic . LNCS , Vol. 2283 . Springer. Tobias Nipkow, Lawrence C. Paulson, and Makarius Wenzel. 2002. Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic . LNCS, Vol. 2283. Springer."},{"key":"e_1_3_2_1_14_1","volume-title":"Graph Theory. Archive of Formal Proofs (April","author":"Noschinski Lars","year":"2013","unstructured":"Lars Noschinski . 2013. Graph Theory. Archive of Formal Proofs (April 2013 ). http:\/\/isa-afp.org\/entries\/Graph_Theory.html, Formal proof development. Lars Noschinski. 2013. Graph Theory. Archive of Formal Proofs (April 2013). http:\/\/isa-afp.org\/entries\/Graph_Theory.html, Formal proof development."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449896"},{"key":"e_1_3_2_1_16_1","volume-title":"Matrices: Theory and Applications","author":"Serre Denis","year":"2002","unstructured":"Denis Serre . 2002 . Matrices: Theory and Applications . Springer . Denis Serre. 2002. Matrices: Theory and Applications. Springer."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"e_1_3_2_1_18_1","volume-title":"Algebraic Numbers in Isabelle\/HOL. In ITP 2016 (LNCS)","volume":"9807","author":"Thiemann Ren\u00e9","year":"2016","unstructured":"Ren\u00e9 Thiemann and Akihisa Yamada . 2016 . Algebraic Numbers in Isabelle\/HOL. In ITP 2016 (LNCS) , Vol. 9807 . 391\u2013408. Ren\u00e9 Thiemann and Akihisa Yamada. 2016. Algebraic Numbers in Isabelle\/HOL. In ITP 2016 (LNCS), Vol. 9807. 391\u2013408."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854073"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02230720"},{"key":"e_1_3_2_1_21_1","volume-title":"Modular Complexity Analysis for Term Rewriting. Logical Methods in Computer Science 10, 1:19","author":"Zankl Harald","year":"2014","unstructured":"Harald Zankl and Martin Korp . 2014. Modular Complexity Analysis for Term Rewriting. Logical Methods in Computer Science 10, 1:19 ( 2014 ), 1\u201334. Harald Zankl and Martin Korp. 2014. Modular Complexity Analysis for Term Rewriting. Logical Methods in Computer Science 10, 1:19 (2014), 1\u201334."}],"event":{"name":"CPP '18: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Los Angeles CA USA","acronym":"CPP '18"},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167103","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167103","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:28Z","timestamp":1750212808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":21,"alternative-id":["10.1145\/3167103","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167103","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}