{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:58:41Z","timestamp":1743141521482,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319948201"},{"type":"electronic","value":"9783319948218"}],"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-94821-8_22","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"370-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Proof Pearl: Constructive Extraction of\u00a0Cycle Finding Algorithms"],"prefix":"10.1007","author":[{"given":"Dominique","family":"Larchey-Wendling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"22_CR1","unstructured":"Cycle detection \u2013 Wikipedia, The Free Encyclopedia. \nhttps:\/\/en.wikipedia.org\/wiki\/Cycle_detection"},{"key":"22_CR2","series-title":"Information Security and Cryptography","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44757-4","volume-title":"The Hash Function BLAKE","author":"J-P Aumasson","year":"2014","unstructured":"Aumasson, J.-P., Meier, W., Phan, R.C.-W., Henzen, L.: The Hash Function BLAKE. ISC. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-44757-4"},{"key":"22_CR3","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Bove, A., Capretta, V.: Modelling general recursion in type theory. Math. Structures Comput. Sci. 15(4), 671\u2013708 (2005). \nhttps:\/\/doi.org\/10.1017\/S0960129505004822","DOI":"10.1017\/S0960129505004822"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers \u2013 an overview. Math. Structures Comput. Sci. 26(1), 38\u201388 (2016). \nhttps:\/\/doi.org\/10.1017\/S0960129514000115","DOI":"10.1017\/S0960129514000115"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Brent, R.P.: An improved Monte Carlo factorization algorithm. BIT Numer. Math. 20(2), 176\u2013184 (1980). \nhttps:\/\/doi.org\/10.1007\/BF01933190","DOI":"10.1007\/BF01933190"},{"key":"22_CR7","unstructured":"Cast\u00e9ran, P.: Utilisation en Coq de l\u2019op\u00e9rateur de description (2007). \nhttp:\/\/jfla.inria.fr\/2007\/actes\/PDF\/03_casteran.pdf"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Coen, C.S., Valentini, S.: General Recursion and Formal Topology. In: PAR-2010, Partiality and Recursion in Interactive Theorem Provers. EPiC Series in Computing, vol. 5, pp. 72\u201383. EasyChair (2012). \nhttps:\/\/doi.org\/10.29007\/hl75","DOI":"10.29007\/hl75"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Dufourd, J.F.: Formal study of functional orbits in finite domains. Theoret. Comput. Sci. 564, 63\u201388 (2015). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2014.10.041","DOI":"10.1016\/j.tcs.2014.10.041"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log. 65(2), 525\u2013549 (2000). \nhttps:\/\/doi.org\/10.2307\/2586554","DOI":"10.2307\/2586554"},{"key":"22_CR11","unstructured":"Filli\u00e2tre, J.C.: Tortoise and the hare algorithm (2007). \nhttps:\/\/github.com\/coq-contribs\/tortoise-hare-algorithm"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Fridlender, D.: An interpretation of the fan theorem in type theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 93\u2013105. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48167-2_7","DOI":"10.1007\/3-540-48167-2_7"},{"key":"22_CR13","unstructured":"Gammie, P.: The Tortoise and Hare Algorithm (2015). \nhttps:\/\/www.isa-afp.org\/entries\/TortoiseHare.html"},{"key":"22_CR14","unstructured":"Joux, A.: Algorithmic Cryptanalysis. Cryptography and Network Security. Chapman & Hall\/CRC (2009)"},{"key":"22_CR15","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms. Addison-Wesley Longman Publishing Co., Inc., Boston (1997)"},{"key":"22_CR16","unstructured":"Lagarias, J.: The Ultimate Challenge: The $$3x+1$$ Problem. American Mathematical Society (2010). \nhttp:\/\/bookstore.ams.org\/mbk-78"},{"key":"22_CR17","unstructured":"Larchey-Wendling, D., Monin, J.F.: Simulating Induction-Recursion for Partial Algorithms. In: TYPES 2018, Braga, Portugal (2018). \nhttps:\/\/members.loria.fr\/DLarchey\/files\/papers\/TYPES_2018_paper_19.pdf"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Pollard, J.M.: A monte carlo method for factorization. BIT Numer. Math. 15(3), 331\u2013334 (1975). \nhttps:\/\/doi.org\/10.1007\/BF01933667","DOI":"10.1007\/BF01933667"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,9,11]],"date-time":"2018-09-11T18:40:04Z","timestamp":1536691204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}