{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:44Z","timestamp":1767929264331,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_15","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"195-210","source":"Crossref","is-referenced-by-count":6,"title":["The Optimal Fixed Point Combinator"],"prefix":"10.1007","author":[{"given":"Arthur","family":"Chargu\u00e9raud","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44659-1_1","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Balaa","year":"2000","unstructured":"Balaa, A., Bertot, Y.: Fix-point equations for well-founded recursion in type theory. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 1\u201316. Springer, Heidelberg (2000)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11737414_9","volume-title":"Functional and Logic Programming","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 114\u2013129. Springer, Heidelberg (2006)"},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1017\/S0960129503004122","volume":"14","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Frade, M.J., Gim\u00e9nez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science\u00a014(1), 97\u2013141 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/11417170_9","volume-title":"Typed Lambda Calculi and Applications","author":"Y. Bertot","year":"2005","unstructured":"Bertot, Y.: Filters on coinductive streams, an application to eratosthenes\u2019 sieve. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 102\u2013115. Springer, Heidelberg (2005)"},{"issue":"5","key":"15_CR5","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/j.entcs.2008.05.018","volume":"203","author":"Yves Bertot","year":"2008","unstructured":"Bertot, Y., Komendantskaya, E.: Inductive and Coinductive Components of Corecursive Functions in Coq. In: Proceedings of CMCS\u201908, April 2008. ENTCS, vol.\u00a0203, pp. 25\u201347 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1389449.1389461","volume-title":"PPDP","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Komendantsky, V.: Fixed point semantics and partial recursion in Coq. In: Antoy, S., Albert, E. (eds.) PPDP, pp. 89\u201396. ACM, New York (2008)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44755-5_10","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Bove","year":"2001","unstructured":"Bove, A., Capretta, V.: Nested general recursion and partiality in type theory. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 121\u2013135. Springer, Heidelberg (2001)"},{"key":"15_CR8","unstructured":"Dubois, C., Donzeau-Gouge, V.: A step towards the mechanization of partial functions: domains as inductive predicates. In: CADE-15 Workshop on mechanization of partial functions (1998)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-39185-1_9","volume-title":"Types for Proofs and Programs","author":"P. Gianantonio Di","year":"2003","unstructured":"Di Gianantonio, P., Miculan, M.: A unifying approach to recursive and co-recursive definitions. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 148\u2013161. Springer, Heidelberg (2003)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-540-24727-2_11","volume-title":"Foundations of Software Science and Computation Structures","author":"P. Gianantonio Di","year":"2004","unstructured":"Di Gianantonio, P., Miculan, M.: Unifying recursive and co-recursive definitions in sheaf categories. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 136\u2013150. Springer, Heidelberg (2004)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-60275-5_66","volume-title":"TPHOLs","author":"J. Harrison","year":"1995","unstructured":"Harrison, J.: Inductive definitions: Automation and application. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) TPHOLs 1995. LNCS, vol.\u00a0971, pp. 200\u2013213. Springer, Heidelberg (1995)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. Journal of Automated Reasoning (to appear, December 2009)","DOI":"10.1007\/s10817-009-9157-2"},{"key":"15_CR13","unstructured":"Krsti\u0107, S.: Inductive fixpoints in higher order logic (February 2004)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/10930755_17","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Krsti\u0107","year":"2003","unstructured":"Krsti\u0107, S., Matthews, J.: Inductive invariants for nested recursion. In: Basin, D.A., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 253\u2013269. Springer, Heidelberg (2003)"},{"key":"15_CR15","unstructured":"Letouzey, P.: Programmation fonctionnelle certifi\u00e9e: L\u2019extraction de programmes dans l\u2019assistant Coq (June 1, 2007)"},{"issue":"3","key":"15_CR16","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1137\/0205033","volume":"5","author":"Z. Manna","year":"1976","unstructured":"Manna, Z., Shamir, A.: The theoretical aspects of the optimal FixedPoint. SIAM Journal on Computing\u00a05(3), 414\u2013426 (1976)","journal-title":"SIAM Journal on Computing"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-48256-3_6","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Matthews","year":"1999","unstructured":"Matthews, J.: Recursive function definition over coinductive types. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 73\u201390. Springer, Heidelberg (1999)"},{"issue":"3","key":"15_CR18","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B. Nordstr\u00f6m","year":"1988","unstructured":"Nordstr\u00f6m, B.: Terminating general recursion. BIT\u00a028(3), 605\u2013619 (1988)","journal-title":"BIT"},{"key":"15_CR19","unstructured":"Slind, K.: Reasoning about Terminating Functional Programs. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset coercions in coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:00Z","timestamp":1606186020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}