{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:37:00Z","timestamp":1725557820898},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540406648"},{"type":"electronic","value":"9783540451303"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_17","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T15:27:09Z","timestamp":1150730829000},"page":"253-269","source":"Crossref","is-referenced-by-count":5,"title":["Inductive Invariants for Nested Recursion"],"prefix":"10.1007","author":[{"given":"Sava","family":"Krsti\u0107","sequence":"first","affiliation":[]},{"given":"John","family":"Matthews","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Andersen, H.R.: An Introduction to Binary Decision Diagrams (Lecture Notes) (October 1997), http:\/\/www.itu.dk\/people\/hra\/bdd97.ps.gz"},{"key":"17_CR2","unstructured":"Balaa, A., Bertot, Y.: Fonctions r\u00e9cursives g\u00e9n\u00e9rales par it\u00e9ration en th\u00e9orie des types. In: Journ\u00e9es francophones des langages applicatifs, JFLA 2002. INRIA (2002)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-45685-6_7","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2002","unstructured":"Bertot, Y., Capretta, V., Barman, K.D.: Type-theoretic functional semantics. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 83\u201398. Springer, Heidelberg (2002)"},{"key":"17_CR4","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)"},{"issue":"8","key":"17_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"issue":"1","key":"17_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1005797629953","volume":"19","author":"J. Giesl","year":"1997","unstructured":"Giesl, J.: Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning\u00a019(1), 1\u201329 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-60275-5_66","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J. Harrison","year":"1995","unstructured":"Harrison, J.: Inductive definitions: Automation and application. In: Schubert, E.T., Windley, P.J., Alves-Foss, J. (eds.) Higher Order Logic Theorem Proving and Its Applications, pp. 200\u2013213. Springer, Berlin (1995)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/BFb0055152","volume-title":"Theorem Proving in Higher Order Logics","author":"F.W. Henke von","year":"1998","unstructured":"von Henke, F.W., et al.: Case Studies in Meta-Level Theorem Proving. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 461\u2013478. Springer, Heidelberg (1998)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Krsti\u0107, S., Matthews, J.: Verifying BDD algorithms through monadic interpretation. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 182\u2013195. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-47813-2_13"},{"issue":"11","key":"17_CR10","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/359863.359885","volume":"20","author":"Z. Manna","year":"1977","unstructured":"Manna, Z., Shamir, A.: The optimal approach to recursive programs. Communications of the ACM\u00a020(11), 824\u2013831 (1977)","journal-title":"Communications of the ACM"},{"key":"17_CR11","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)"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1016\/0020-0190(79)90063-2","volume":"9","author":"J.S. Moore","year":"1979","unstructured":"Moore, J.S.: A mechanical proof of the termination of Takeuchi\u2019s function. Information Processing Letters\u00a09, 176\u2013181 (1979)","journal-title":"Information Processing Letters"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S095679689900341X","volume":"9","author":"O. M\u00fcller","year":"1999","unstructured":"M\u00fcller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming\u00a09, 191\u2013223 (1999)","journal-title":"Journal of Functional Programming"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"M\u00fcller, O., Slind, K.: Treating partiality in a logic of total functions. The Computer Journal\u00a040(10) (1997)","DOI":"10.1093\/comjnl\/40.10.640"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1","key":"17_CR16","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/BF00246023","volume":"2","author":"L.C. Paulson","year":"1986","unstructured":"Paulson, L.C.: Proving termination of normalization functions for conditional expressions. Journal of Automated Reasoning\u00a02(1), 63\u201374 (1986)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BFb0105417","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1996","unstructured":"Slind, K.: Function definition in higher order logic. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 381\u2013397. Springer, Heidelberg (1996)"},{"key":"17_CR18","unstructured":"Slind, K.: Reasoning about Terminating Functional Programs. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/3-540-44659-1_31","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2000","unstructured":"Slind, K.: Another look at nested recursion. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 498\u2013518. Springer, Heidelberg (2000)"},{"key":"17_CR20","unstructured":"Sumners, R.: Correctness proof of a BDD manager in the context of satisfiability checking. Technical Report TR-00-29, The University of Texas at Austin, Department of Computer Sciences (2000)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-44464-5_13","volume-title":"Advances in Computing Science - ASIAN 2000","author":"K.N. Verma","year":"2000","unstructured":"Verma, K.N., et al.: Reflecting BDDs in Coq. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol.\u00a01961, pp. 162\u2013181. Springer, Heidelberg (2000)"},{"key":"17_CR22","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: an Introduction","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: an Introduction. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T15:39:38Z","timestamp":1586965178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/10930755_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}