{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:39Z","timestamp":1775790759504,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540581567","type":"print"},{"value":"9783540484677","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_11","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:21:10Z","timestamp":1330269670000},"page":"148-161","source":"Crossref","is-referenced-by-count":28,"title":["A fixedpoint approach to implementing (Co)inductive definitions"],"prefix":"10.1007","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"11_CR1","unstructured":"Abramsky, S., The lazy lambda calculus. In Resesarch Topics in Functional Programming, D. A. Turner, Ed. Addison-Wesley, 1977, pp. 65\u2013116"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Aczel, P., An introduction to inductive definitions, In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, 1977, pp. 739\u2013782","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"11_CR3","unstructured":"Aczel, P., Non-Well-Founded Sets, CSLI, 1988"},{"key":"11_CR4","unstructured":"Boyer, R. S., Moore, J. S., A Computational Logic, Academic Press, 1979"},{"key":"11_CR5","unstructured":"Camilleri, J., Melham, T. F., Reasoning with inductively defined relations in the HOL theorem prover. Tech. Rep. 265, Comp. Lab., Univ. Cambridge, August 1992"},{"key":"11_CR6","unstructured":"Davey, B. A., Priestley, H. A., Introduction to Lattices and Order, Cambridge Univ. Press, 1990"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Dybjer, P., Inductive sets and families in Martin-Lofs type theory and their set-theoretic semantics. In Logical Frameworks. G. Huet, G. Plotkin, Eds. Cambridge Univ. Press. 1991, pp. 280\u2013306","DOI":"10.1017\/CBO9780511569807.012"},{"issue":"2","key":"11_CR8","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"Farmer, W. M., Guttman, J. D., Thayer, F. J., IMPS: An interactive mathematical proof system, J. Auto. Reas. 11, 2 (1993), 213\u2013248","journal-title":"J. Auto. Reas."},{"key":"11_CR9","unstructured":"Hennessy, M., The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics, Wiley, 1990"},{"key":"11_CR10","unstructured":"Huet, G., Induction principles formalized in the Calculus of Constructions, In Programming of Future Generation Computers (1988), Elsevier, pp. 205\u2013216"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Melham, T. F., Automating recursive type definitions in higher order logic. In Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle, P. A. Subrahmanyam, Eds. Springer, 1989, pp. 341\u2013386","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"11_CR12","unstructured":"Milner, R., How to derive inductions in LCF, note, Dept. Comp. Sci., Univ. Edinburgh, 1980"},{"key":"11_CR13","unstructured":"Milner, R., Communication and Concurrency, Prentice-Hall, 1989"},{"key":"11_CR14","unstructured":"Monahan, B. Q., Data Type Proofs using Edinburgh LCF, PhD thesis, University of Edinburgh, 1984"},{"key":"11_CR15","unstructured":"Paulin-Mohring, C., Inductive definitions in the system Coq: Rules and properties, Research Report 92-49, LIP, Ecole Normale Sup\u00e9rieure de Lyon, Dec. 1992"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Paulson, L. C., Logic and Computation: Interactive proof with Cambridge LCF, Cambridge Univ. Press, 1987","DOI":"10.1017\/CBO9780511526602"},{"key":"11_CR17","unstructured":"Paulson, L. C., ML for the Working Programmer, Cambridge Univ. Press, 1991"},{"key":"11_CR18","unstructured":"Paulson, L. C., Co-induction and co-recursion in higher-order logic, Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993"},{"key":"11_CR19","unstructured":"Paulson, L. C., Introduction to Isabelle, Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993"},{"issue":"3","key":"11_CR20","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\u2013389","journal-title":"J. Auto. Reas."},{"key":"11_CR21","unstructured":"Paulson, L. C., Set theory for verification: II. Induction and recursion, Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993"},{"key":"11_CR22","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":"11_CR23","doi-asserted-by":"crossref","unstructured":"Pitts, A. M., A co-induction principle for recursively defined domains, Theoretical Comput. Sci. (1994), In press; available as Report 252, Comp. Lab., Univ. Cambridge","DOI":"10.1016\/0304-3975(94)90014-0"},{"key":"11_CR24","unstructured":"Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I., An EVES data abstraction example, In FME '93: Industrial-Strength Formal Methods (1993), J. C. P. Woodcock, P. G. Larsen, Eds., Springer, pp. 578\u2013596, LNCS 670"},{"key":"11_CR25","unstructured":"Szasz, N., A machine checked proof that Ackermann's function is not primitive recursive, In Logical Environments, G. Huet, G. Plotkin, Eds. Cambridge Univ. Press, 1993, pp. 317\u2013338"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:31Z","timestamp":1605647851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}