{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:59:33Z","timestamp":1760079573381},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105417","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T16:17:00Z","timestamp":1320855420000},"page":"381-397","source":"Crossref","is-referenced-by-count":24,"title":["Function definition in higher-order logic"],"prefix":"10.1007","author":[{"given":"Konrad","family":"Slind","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1093\/comjnl\/38.2.121","volume":"38","author":"S. Agerholm","year":"1995","unstructured":"S. Agerholm. LCF examples in HOL. The Computer Journal, 38(2):121\u2013130, July 1995.","journal-title":"The Computer Journal"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"S. Agerholm. Non-primitive recursive function definition. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications (LNCS 971), pages 17\u201331, Aspen Grove, Utah, September 1995. Springer Verlag.","DOI":"10.1007\/3-540-60275-5_54"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Lennart Augustsson. Compiling pattern matching. In J.P. Jouannaud, editor, Conference on Functional Programming Languages and Computer Architecture (LNCS 201), pages 368\u2013381, Nancy, France, 1985.","DOI":"10.1007\/3-540-15975-4_48"},{"key":"25_CR4","unstructured":"Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, 1979."},{"key":"25_CR5","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185\u2013253, 1993.","journal-title":"Artificial Intelligence"},{"key":"25_CR6","unstructured":"Simon Finn, Mike Fourman, and John Longley. Partial functions in a total setting. To appear in Journal of Automated Reasoning, 1996."},{"key":"25_CR7","volume-title":"Proceedings of the 2nd International Static Analysis Symposium","author":"J. Giesl","year":"1995","unstructured":"Juergen Giesl. Termination analysis for functional programs using term orderings. In Proceedings of the 2nd International Static Analysis Symposium, Glasgow, Scotland, 1995. Springer-Verlag."},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"H. Busch. Unification based induction. In L.J.M. Claesen and M.J.C. Gordon, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 97\u2013116, Leuven, Belgium, September 1992. IFIP TC10\/WG10.2, North-Holland. IFIP Transactions.","DOI":"10.1016\/B978-0-444-89880-7.50013-9"},{"issue":"2","key":"25_CR9","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/comjnl\/38.2.131","volume":"38","author":"P. V. Homeier","year":"1995","unstructured":"P. V. Homeier and D. F. Martin. A verified verification condition generator. The Computer Journal, 38(2):131\u2013141, July 1995.","journal-title":"The Computer Journal"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Peter Johnstone. Notes on logic and set theory. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9781139172066"},{"issue":"4","key":"25_CR11","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1006\/inco.1996.0004","volume":"124","author":"D. Kesner","year":"1996","unstructured":"Delia Kesner, Laurence Puel, and Val Tannen. A typed pattern calculus. Information and Computation, 124(4):32\u201361, 1996.","journal-title":"Information and Computation"},{"key":"25_CR12","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-58085-9_78","volume-title":"Types for Proofs and Programs (LNCS 806)","author":"L. Magnusson","year":"1994","unstructured":"Lena Magnusson and Bengt Nordstrom. The ALF proof editor and its proof engine. In Types for Proofs and Programs (LNCS 806), pages 213\u2013237, Nijmegen, Netherlands, 1994. Springer-Verlag."},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Pascal Manoury. A user's friendly syntax to define recursive functions as typed \u03bb-terms. In Types for Proofs and Programs: International Workshop TYPES'94, number 996 in Lecture Notes in Computer Science, Baastad, Sweden, June 1995. Springer Verlag.","DOI":"10.1007\/3-540-60579-7_5"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Pascal Manoury and Marianne Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science, (135):319\u2013343, 1994.","DOI":"10.1016\/0304-3975(94)00021-2"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Tom Melham. Automating recursive type definitions in higher order logic. In Graham Birtwistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341\u2013386. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"25_CR16","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/BF01887212","volume":"1","author":"T. Nipkow","year":"1989","unstructured":"Tobias Nipkow. Term rewriting and beyond\u2014theorem proving in Isabelle. Formal Aspects of Computing, 1:320\u2013338, 1989.","journal-title":"Formal Aspects of Computing"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B. Nordstrom","year":"1988","unstructured":"Bengt Nordstrom. Terminating general recursion. BIT, 28:605\u2013619, 1988.","journal-title":"BIT"},{"key":"25_CR18","series-title":"LNAI","first-page":"748","volume-title":"11th International Conference on Automated Deduction","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, LNAI 607, pages 748\u2013752, Saratoga Springs, New York, USA, June 15\u201318, 1992. Springer-Verlag."},{"key":"25_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. Paulson","year":"1983","unstructured":"Lawrence Paulson. A higher order implementation of rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"},{"key":"25_CR20","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/S0747-7171(86)80002-5","volume":"2","author":"L. Paulson","year":"1986","unstructured":"Lawrence Paulson. Constructing recursion operators in intuitionistic type theory. Journal of Symoblic Computation, 2:325\u2013355, 1986.","journal-title":"Journal of Symoblic Computation"},{"key":"25_CR21","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/BF00246023","volume":"2","author":"L. Paulson","year":"1986","unstructured":"Lawrence Paulson. Proving termination of normalization functions for conditional expressions. Journal of Automated Reasoning, 2:63\u201374, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR22","unstructured":"Franz Regensburger. HOLCF: Eine konservative Einbettung von LCF in HOL. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1994."},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"H. Schwichtenberg and S. Wainer. Ordinal bounds for programs. In Jeff Remmel, editor, Feasible Mathematics II, pages 387\u2013406. Birkh\u00e4user, 1994.","DOI":"10.1007\/978-1-4612-2566-9_13"},{"key":"25_CR24","unstructured":"M. van der Voort. Introducing well-founded function definitions in HOL. Leuven, Belgium, September 1992. IFIP TC10\/WG10.2, Elsevier Science Publishers."},{"issue":"1","key":"25_CR25","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"Christoph Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71(1):101\u2013157, 1994.","journal-title":"Artificial Intelligence"}],"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\/BFb0105417","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T05:44:36Z","timestamp":1560923076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105417"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0105417","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}