{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:44Z","timestamp":1761611144550},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bf00881916","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:40:00Z","timestamp":1104003600000},"page":"167-215","source":"Crossref","is-referenced-by-count":39,"title":["Set theory for verification. II: Induction and recursion"],"prefix":"10.1007","volume":"15","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"CR1","first-page":"65","volume-title":"Research Topics in Functional Programming","author":"S. Abramsky","year":"1977","unstructured":"Abramsky, S.: The lazy lambda calculus, in D. A. Turner, (ed.)Research Topics in Functional Programming, Addison-Wesley, Reading, MA, 1977, pp. 65?116."},{"key":"CR2","unstructured":"Aczel, P.:Non-Well-Founded Sets, CSLI, 1988."},{"key":"CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"Bledsoe, W. W.: Non-resolution theorem proving,Art. Intel. 9 (1977), 1?35.","journal-title":"Art. Intel."},{"key":"CR4","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"Boyer, R. S. and Moore, J. S.:A Computational Logic, Academic Press, New York, 1979."},{"key":"CR5","unstructured":"Camilleri, J. and Melham, T. F.: Reasoning with inductively defined relations in the HOL theorem prover, Tech. Rep. 265, Comp. Lab., Univ. Cambridge, 1992."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Coquand, T. and Paulin, C.: Inductively defined types, inCOLOG-88: International Conference on Computer Logic, LNCS 417, Springer, 1990, pp. 50?66.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"CR7","unstructured":"Davey, B. A. and Priestley, H. A.:Introduction to Lattices and Order, Cambridge Univ. Press, 1990."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Devlin, K. J.:Fundamentals of Contemporary Set Theory, Springer, 1979.","DOI":"10.1007\/978-1-4684-0084-7"},{"key":"CR9","unstructured":"Girard, J.-Y.:Proofs and Types, Translated by Yves LaFont and Paul Taylor, Cambridge Univ. Press, 1989."},{"key":"CR10","unstructured":"Givan, R., McAllester, D., Witty, C. and Zalondek, K.: Ontic: Language specification and user's manual, Tech. Rep., MIT, 1992, Draft 4."},{"key":"CR11","volume-title":"Naive Set Theory","author":"P. R. Halmos","year":"1960","unstructured":"Halmos, P. R.:Naive Set Theory, Van Nostrand, New York, 1960."},{"issue":"1","key":"CR12","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/0167-6423(81)90004-6","volume":"1","author":"Z. Manna","year":"1981","unstructured":"Manna, Z. and Waldinger, R.: Deductive synthesis of the unification algorithm,Sci. Comput. Programming 1(1) (1981), 5?48.","journal-title":"Sci. Comput. Programming"},{"key":"CR13","unstructured":"Martin-L\u00f6f, P.:Intuitionistic Type Theory, Bibliopolis, 1984."},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"McDonald, J. and Suppes, P.: Student use of an interactive theorem prover, In W. W. Bledsoe and D. W. Loveland (eds),Automated Theorem Proving: After 25 Years, American Mathematical Society, 1984, pp. 315?360.","DOI":"10.1090\/conm\/029\/16"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Melham, T. F.: Automating recursive type definitions in higher order logic, in G. Birtwistle and P. A. Subrahmanyam (eds),Current Trends in Hardware Verification and Automated Theorem Proving, Springer, 1989, pp. 341?386.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"CR16","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.:Communication and Concurrency, Prentice-Hall, Englewood Cliffs, NJ, 1989."},{"key":"CR17","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M. and Harper, R.:The Definition of Standard ML, MIT Press, Cambridge, MA, 1990."},{"issue":"1","key":"CR18","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BF00881863","volume":"10","author":"P. No\u00ebl","year":"1993","unstructured":"No\u00ebl, P.: Experimenting with Isabelle in ZF set theory,J. Auto. Reas. 10(1) (1993), 15?58.","journal-title":"J. Auto. Reas."},{"key":"CR19","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B. Nordstr\u00f6m","year":"1988","unstructured":"Nordstr\u00f6m, B.: Terminating general recursion,BIT 28 (1988), 605?619.","journal-title":"BIT"},{"key":"CR20","unstructured":"Nordstr\u00f6m, B., Petersson, K. and Smith, J.:Programming in Martin-L\u00f6f's Type Theory, An Introduction, Oxford University Press, 1990."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1016\/S0747-7171(86)80002-5","volume":"2","author":"L. C. Paulson","year":"1986","unstructured":"Paulson, L. C.: Constructing recursion operators in intuitionistic type theory,J. Symb. Comput. 2 (1986) 325?355.","journal-title":"J. Symb. Comput."},{"issue":"3","key":"CR22","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L. C. Paulson","year":"1993","unstructured":"Paulson, L. C.: Set theory for verification: I. From foundations to functions,J. Auto. Reas. 11(3) (1993), 353?389.","journal-title":"J. Auto. Reas."},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: A concrete final coalgebra theorem for ZF set theory, Tech. Rep., Comp. Lab., Univ. Cambridge, 1994.","DOI":"10.1007\/3-540-60579-7_7"},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: A fixedpoint approach to implementing (co)inductive definitions, in A. Bundy (ed.),12th Conf. Auto. Deduct., LNAI 814, Springer, 1994, pp. 148?161.","DOI":"10.1007\/3-540-58156-1_11"},{"key":"CR25","unstructured":"Schroeder-Heister, P.: Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ?, ?, ?, ?, ?, inComputation and Proof Theory: Logic Colloquium '83, Lecture Notes in Math. 1104, Springer, 1984, pp. 399?426."},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"Smith, J.: The identification of propositions and types in Martin-L\u00f6f's type theory: A programming example, in M. Karpinski (ed.),Foundations of Computation Theory, LNCS 158, Springer, 1983, pp. 445?456.","DOI":"10.1007\/3-540-12689-9_125"},{"key":"CR27","volume-title":"Axiomatic Set Theory","author":"P. Suppes","year":"1972","unstructured":"Suppes, P.:Axiomatic Set Theory, Dover, New York, 1972."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881916.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881916\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881916","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:30:09Z","timestamp":1586043009000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881916"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF00881916"],"URL":"https:\/\/doi.org\/10.1007\/bf00881916","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}